Skip to content
| Marketplace
Sign in
Visual Studio Code>Programming Languages>Motoko-sanNew to Visual Studio Code? Get it now.
Motoko-san

Motoko-san

DFINITY Foundation

|
1,356 installs
| (0) | Free
Experimental formal verification support for Motoko
Installation
Launch VS Code Quick Open (Ctrl+P), paste the following command, and press enter.
Copied to clipboard
More Info

Important note: This is an experimental fork of the official Motoko VS Code extension. Please disable the official extension if you run into any unexpected behavior.

Motoko-san

Experimental formal verification support for Motoko.

Visual Studio Marketplace PRs Welcome

Background

Motoko is a high-level smart contract language for the Internet Computer.

This extension makes it possible to write code specifications (such as actor-level invariants) for Motoko programs. The assertions are automatically checked, at compile time, by Viper Viper, a formal verifier developed at ETH Zurich.

Usage

To enable formal verification, insert // @verify at the top of your Motoko file.

Example

// @verify

actor {

  var claimed = false;

  var count = 0 : Int;

  assert:invariant count == 0 or count == 1;
  assert:invariant not claimed implies count == 0;

  public shared func claim() : async () {
    if (not claimed) {
      claimed := true;

      await async {
        assert:1:async (claimed and count == 0);
        count += 1;
      };
    };
  };

}

Building from Source

  • Clone vscode-motoko with following command: git clone https://github.com/dfinity/vscode-motoko -b viper --recurse-submodules
  • In your terminal, run cd vscode-motoko
  • Install the npm modules needed as dependencies: npm install
  • Run npm run package (this will rebuild the compiler bindings)
  • Right-click the generated /motoko-viper-*.vsix file and select "Install extension VSIX"

Tracking dfinity/motoko

The submodule motoko usually tracks the master branch of the official Motoko repo and needs periodical updates here to adjust the pin in order to absorb features and bugfixes. Execute the following commands from toplevel to obtain updates:

git branch --show-current
git submodule update --remote
git diff
git commit -am 'track `motoko` ToT'
git push

Further reading

A more detailed overview of Motoko-san is available here.

  • Contact us
  • Jobs
  • Privacy
  • Manage cookies
  • Terms of use
  • Trademarks
© 2025 Microsoft