Motoko-san: Code-Level Verification in Motoko

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

19 Likes

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

5 Likes

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 :cry:

2 Likes

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:

Happy to release a bugfix if needed.

Thanks for the help. I’ve tried again this morning, I checked the logs but everything seems fine to me. I copy pasted them here (I activated the verbose version) : MotokoSanSandbox/MotokoLanguageServer.log at main · sardariuss/MotokoSanSandbox · GitHub

Something strange is when I try to restart the motoko language server I get:
image

2 Likes

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!

1 Like

I had it disabled, I uninstalled it but it’s still the same diagnostic. Sure, I am not in a hurry anyway :slight_smile: 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. :slight_smile:

3 Likes