Motoko-san: Code-Level Verification in Motoko

Developers
1

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

13 Likes
2

This is such a cool feature!! It feels like a very succinct mechanism to guard against states which should be impossible, and if it were fully developed it could replace categories of testing that would otherwise be required.

Having a way to highlight reentrancy vulnerabilities is fantastic, as it’s one of the most common (and dangerous!) pitfalls of canister development. Looking forward to trying it out, and hoping to see if develop into production ready tool! :star_struck:

p.s. motoko-san is a great name

4 Likes