Creusot helps you prove your Rust code is correct

github.com

66 points·fanf2··9 comments

I'm super interested in this sort of stuff, but I have a hard time figuring out where to get started. Like, could this help in a typical CRUD application? What sorts of problems is it super useful for? What's a good way to get started integrating it into existing software, or is it better to design software ground-up to be verified? Are there limitations, or certain standard library features that are/aren't supported?

(Not specifically for Creusot)

A decent amount of mission-critical software undergoes formal verification, like spacecraft flight software (my area of expertise). SparkADA lives on because of not just its safety, but formal verifiability.

Interesting, how common is this vs just unit testing? How do you avoid formally verifying something against a spec that could subtly fail in production?

Make sure the specifications can’t fail by verifying them for correctness.

Something like TLA+[1] and Quint[2] specifications can be verified for correctness using Apalache[3]. Then test the Rust code against the specifications using quint_connect.[4]

[1] https://www.learntla.com/

[2] https://quint.sh/

[3] https://apalache-mc.org/

[4] https://docs.rs/quint-connect/latest/quint_connect/

it's generally another layer on top of things like unit testing, MC/DC coverage, etc. not all programs use formal verification though.

How does this differ from https://github.com/verus-lang/verus

Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html).

Verus encodes directly to SMT.

Creusot may gain some more automation perhaps from this approach.

I like the name[0][1].

[0]: https://www.britannica.com/place/Le-Creusot

[1]: https://en.wikipedia.org/wiki/Le_Creusot

Fantastic work

Reply on news.ycombinator.com