This VS Code extension provides interactive IDE features for Viper — the Verification Infrastructure for Permission-based Reasoning.
The extension automatically downloads and manages Viper (via publicly available links, as listed here: http://viper.ethz.ch/downloads/).
Viper IDE uses an open-source 64-bit Java server, so you need Java installed to be able to run it.
Please always refer to the official installation instructiuons for more details (in particular, about defferent operating system support).
If you would like to learn more about Viper, please start with our extensive tutorial.
Lizard is a (visual) verification debugger prototype for Viper IDE. It aims at simplifying the understanding of verification failures by converting SMT models to counterexample diagrams that are shown next to the code.