# Motoko-san: Code-Level Verification in Motoko **URL:** \ **Category:** Developers\ **Created:** [January 25, 2023, 10:49am UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171 "2023-01-25T10:49:42Z")\ **Posts on this page:** 8\ **Page:** 1
**Author:** ![aterga](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/aterga/32/4143_2.png) [@aterga](https://forum.dfinity.org/u/aterga)\ **Post date:** [January 25, 2023, 10:49am UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/1 "2023-01-25T10:49:42Z")
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_](https://marketplace.visualstudio.com/items?itemName=dfinity-foundation.motoko-viper), 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](https://medium.com/@dfinity/developer-grant-for-code-level-verification-in-motoko-37356a095e3c) 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](https://github.com/dfinity/grant-rfps/issues/26) ---
**Author:** ![jorgenbuilder](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/jorgenbuilder/32/22166_2.png) [@jorgenbuilder](https://forum.dfinity.org/u/jorgenbuilder)\ **Post date:** [January 27, 2023, 7:05pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/2 "2023-01-27T19:05:48Z")
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! 🤩 p.s. motoko-san is a great name ---
**Author:** ![sardariuss](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/sardariuss/32/39258_2.png) [@sardariuss](https://forum.dfinity.org/u/sardariuss)\ **Post date:** [March 17, 2023, 2:29pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/3 "2023-03-17T14:29:21Z")
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 😢 ---
**Author:** ![rvanasa](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rvanasa/32/23650_2.png) [@rvanasa](https://forum.dfinity.org/u/rvanasa)\ **Post date:** [March 17, 2023, 11:53pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/4 "2023-03-17T23:53:09Z")
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: ![image](https://us1.discourse-cdn.com/flex023/uploads/dfn/original/2X/8/8bbf4c31640d117b61c3f0a78fc9a1a5da1e5102.png) Happy to release a bugfix if needed. ---
**Author:** ![sardariuss](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/sardariuss/32/39258_2.png) [@sardariuss](https://forum.dfinity.org/u/sardariuss)\ **Post date:** [March 18, 2023, 1:51pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/5 "2023-03-18T13:51:27Z")
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](https://github.com/sardariuss/MotokoSanSandbox/blob/main/MotokoLanguageServer.log) Something strange is when I try to restart the motoko language server I get: ![image](https://us1.discourse-cdn.com/flex023/uploads/dfn/original/2X/a/aecb35247c07bc03ef549c3c241950ee50c1460f.png) ---
**Author:** ![rvanasa](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rvanasa/32/23650_2.png) [@rvanasa](https://forum.dfinity.org/u/rvanasa)\ **Post date:** [March 18, 2023, 8:16pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/6 "2023-03-18T20:16:47Z")
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! ---
**Author:** ![sardariuss](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/sardariuss/32/39258_2.png) [@sardariuss](https://forum.dfinity.org/u/sardariuss)\ **Post date:** [March 19, 2023, 3:37pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/7 "2023-03-19T15:37:04Z")
I had it disabled, I uninstalled it but it’s still the same diagnostic. Sure, I am not in a hurry anyway 🙂 Cheers! ---
**Author:** ![rvanasa](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rvanasa/32/23650_2.png) [@rvanasa](https://forum.dfinity.org/u/rvanasa)\ **Post date:** [April 11, 2023, 3:49pm UTC](https://forum.dfinity.org/t/motoko-san-code-level-verification-in-motoko/18171/8 "2023-04-11T15:49:18Z")
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. 🙂