Add Tool: Creusot

[Lysxia]

Tool Name

Creusot

Description

Creusot is a deductive verifier for Rust. It provides a specification language for contracts (pre/post-conditions, loop invariants, assertions) and enables SMT-based verification via a translation to Coma, an intermediate language which is part of the Why3 platform.

While in its early days, Creusot aimed for the verification of safe code, we have recently added linear ghost types, a feature pioneered by Verus to enable the verification of unsafe low-level pointer-manipulating code. This makes Creusot suitable for several of the std-lib verification challenges.

Tool Information

• Does the tool perform Rust verification? Yes.
• Does the tool deal with unsafe Rust code? Yes.
• Does the tool run independently in CI? Yes.
• Is the tool open source? Yes (modulo solvers, see below).
• Is the tool under development? Yes.
• Will you or your team be able to provide support for the tool? Yes.

Comparison to Other Approved Tools

As a deductive verification tool, Creusot is most similar to VeriFast and Flux among the previously accepted tools.
One notable difference with VeriFast is that it is based on separation logic, while Creusot is not, only using first-order logic. We rely on Rust's type system to guarantee separation properties. In comparison with Flux, one technical difference is the representation of mutable borrows. I would expect the workflow to be quite similar as Flux and Creusot are both SMT-based tools.

Licenses

• Creusot and Why3 (our backend) are licensed under LGPL-2.1.
• Why3find and Z3 are licensed under MIT. CVC4, CVC5 are licensed under BSD-3.
• Alt-ergo (another of the solvers we use) is licensed under the OCamlPro Non-Commercial license

We are currently unsure if that conflicts with the usage in verify-std-rust proposed here.

Steps to Use the Tool

Installation details TBD (should be similar to Flux)

1. cargo creusot prove

Artifacts & Audit Mechanisms

Creusot is implemented in Rust, subject to the common caveats of a non-foundational implementation:
there may be bugs in the implementation, and there may be soundness holes in the theory.

Mitigating measures:

• Creusot is based on prior work, RustHornBelt, which mechanized a soundness proof of a model of mutable borrows with prophecies. Of course, several extensions have been necessary to support the many features of the real-world language that is Rust, and they could introduce new holes. Our team is actively working on formalizing such subtle feature interactions.
• Creusot has an extensive test suite, including several full-fledged algorithms.

Published work:

• Creusot: a foundry for the deductive verification of Rust programs (Xavier Denis, Jacques-Henri Jourdan, Claude Marché, in ICFEM 2022).
• CreuSAT, a SAT solver formally verified with Creusot,
  (Sarek Skotåm, thesis).

Versioning

As Creusot depends on Rustc compiler libraries, it is tied to specific nightly versions.
We will commit to keep up with nightly dependencies often to help maintain proofs in the verify-rust-std repository.
Given how often these updates happen, our plan is to point the verify-rust-std CI to specific commits of the Creusot source repository. We can also tag our own nightly releases if that's preferable.

CI

1. Install

   • Download Creusot sources
   • Use the OCaml github action to obtain Opam (the OCaml package manager)
   • Install Creusot and auxiliary tools (install Why3, Why3find with Opam, download SMT solvers)

2. Verify

   • cargo creusot prove

(For reference, here is Creusot's own CI script)

[Lysxia]

So the one question I have is: are the licenses of Creusot and our dependencies in conflict with their addition to verify-rust-std? It's unclear to me what the modalities of verify-rust-std are. AFAICT the intended usage is to install and run the tool in CI, and this is not an artifact meant for distribution. But I'm not familiar with legal subtleties.

[tautschnig]

We will seek out guidance with regard to the licenses and will get back to you.