Creusot IDE

A VS Code extension providing support for Creusot, a deductive verifier for Rust code.

This project is work in progress. An official release is upcoming.

Install Creusot IDE

Creusot itself should be installed separately.

Creusot IDE consists of two parts:

1. The Creusot IDE extension, installed via VS Code: open VS Code > Extensions > Search "Creusot IDE".

2. The Creusot LSP language server, which must currently be installed separately:

    git clone https://github.com/creusot-rs/creusot-ide
    opam pin creusot-lsp creusot-ide/
    # Say yes to install creusot-lsp
   

   Creusot LSP currently depends on development versions of Why3 and Why3find. (Tested with Why3 commit 9c0548a62 and Why3find commit 7f728e9 + temporary local patch)

    git clone https://gitlab.inria.fr/why3/why3
    opam pin why3 why3#9c0548a62
   
    git clone https://git.frama-c.com/pub/why3find
    cd why3find
    git checkout 7f728e9
    git apply ../creusot-ide/why3find.patch
    git commit -am "patch"
    opam pin why3find .
    cd ..
   

Features

Creusot IDE helps you nagivate between your Rust sources and the verification artifacts generated by Creusot and Why3find.

• Run and inspect proofs from within the editor.
  • Functions with proof obligations will have a button in the gutter to their left. Click to run the prover (why3find prove). Alt+click to start Why3 IDE (only if the prover fails).
• Links in your editor between fragments of Rust code and their counterparts in the generated Coma and proof files.
• Display hypotheses and goal at various point of the proof.
• Syntax highlighting:
  • .rs files: Creusot-specific attributes and Pearlite expressions,
  • .coma files.

Settings

• creusot.lspPath: Path to the creusot-lsp executable. Default: "", to find the executable in PATH.

Known issues

Compatibility with standard Rust tools (Rust analyzer, etc.)

• How to build projects verified by Creusot.

  Creusot implicitly enables some unstable features to verify programs. When building programs with cargo build, they must be enabled explicitly with the following attribute in the root lib.rs:

  #![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]

  Linters will then warn that creusot is an unknown parameter. To silence the warning, add this option to Cargo.toml:

  [lints.rust]
  unexpected_cfgs = { level = "warn", check-cfg = ['cfg(creusot)'] }

  This issue is being tracked at creusot-rs/creusot#1000

• Rust analyzer doesn't know how to parse Creusot specifications (attributes such as ensures, etc.), so they are underlined in red.

  Add this option in settings.json:

  "rust-analyzer.check.overrideCommand": [
          "cargo",
          "creusot",
          "--",
          "--message-format=json"
      ]