Credits

Creusot is powered by the following projects:

• Rust

• Why3

• Why3find

• SMT Solvers:

  • Alt-ergo
  • Z3
  • CVC5, CVC4

Contract-based verification: a big family

Creusot is but one in a long line of formal verification tools, going all the way back to the fundamental idea of Floyd-Hoare logic.

The following is far from an exhaustive list of related tools.

For Rust:

• Verus
• Aeneas
• Hax
• Flux
• Refined Rust
• Verifast
• Prusti

Other languages:

• WhyML
• SPARK Ada
• Frama-C
• F*