Safety-Critical Tool Submission: creusot

[af-airbus]

What is the name of the tool?

creusot

What is a description of the tool, what it does, how it would be used?

Creusot is a deductive verifier for Rust code. It verifies your code is safe from panics, overflows, and assertion failures. By adding annotations you can take it further and verify your code does the correct thing.

Creusot works by translating Rust code to Coma, an intermediate verification language of the Why3 Platform. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!

Link to the tool repo or homepage

https://github.com/creusot-rs/creusot

What is your role/connection to this tool?

Other

Tool category

formal-verification