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 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!
Hey thank you very much for this, I’ve been coding in Motoko for a little while and I learned a lot just by reading your articles.
Unfortunatly I don’t manage to make the extension quite work on my setup. I run dfx on wsl, and I use the wsl extension in VS code. I got a main.mo.vpr file that gets updated and verified when I update my canister code, but I don’t manage to get the errors displayed in motoko code itself. Is it because it requires the Error Lens extension ? But it’s not available on WSL
It should be possible to view errors in the Motoko file without the Error Lens extension. Does anything look unusual in your “Motoko Language Server” output logs? Here’s a screenshot to clarify where to find this in VS Code:
Do you happen to have both the “Motoko” and “Motoko-san” extensions installed at the same time? If so, try deactivating the “Motoko” extension. These extensions are incompatible with each other, so loading both will often cause of the error message in your screenshot. If this isn’t the case, I will try to reproduce the issue on my Windows machine as soon as possible (currently traveling). Cheers!
Motoko-san now supports WSL as of version 0.1 of the extension. Let me know if this ends up fixing the error messages (and lack thereof) that you were encountering before.
Cheers!