Once opam installed:
$ opam install archetype
Please refer to this page to download and install VS code.
Install through VS Code extensions. Search for
Can also be installed with VS Code Quick Open: press
Cmd/Ctrl + P, paste the following command, and press enter.
ext install edukera.archetype
The vscode extension is configured via the normal vscode settings screen.
Archetype generates Why3 file format (mlw) for contract verification purpose.
The current version of why3 is 1.3.3. It is installed with opam:
$ opam install why3
You also need to install the Why3 IDE (interface) (currently 1.3.3):
$ opam install why3-ide
The IDE uses GTK library that may need to be installed with the proper system-dependent package management system (
apt for linux,
brew for mac os, ...).
Why3 itself generates contracts' proof obligations and transcodes them to several SMT solvers languages.
Each solver needs to be installed separately. Once the solvers are installed (see below), they need to be detected by Why3 with the following command:
$ why3 config --detect-provers
Alt-ergo is developed by LRI, where Why3 also comes from. The currently supported version is 2.3.1.
$ opam install alt-ergo.2.3.1
CVC4 is developed at Stanford. The currently supported version is 1.7. Download the binary at the following page:
Z3 is developped by Microsoft. The currently supported version is 4.7.1. Download the binary at the following page: