We believe that code-level verification would be extremely beneficial to all Web3 projects, particularly high-stake applications like DeFi. Late last year, a few formal verification experts from the DFINITY Foundation came together to prototype Motoko-san, a formal, automated, code-level verifier for the Motoko smart contract language.
Conceptually, Motoko-san enables developers to leverage automatic verification to build bug-free, Web3 applications in Motoko. The current implementation is sufficient for demonstration purposes, but not for real-world applications, as the set of supported language features is minimal.
We are now sharing Motoko-san with the community and announcing our willingness to support a team that would be interested to build a more complete verifier based on our prototype.
This thread is dedicated to discussing code-level verification in Motoko, also beyond the Motoko-san tool. If you haven’t already, please read our latest Medium post on the subject. For more details on the grant proposal, please see RFP-6: Automated Code-Level Verifier for Motoko · Issue #26 · dfinity/grant-rfps · GitHub