3 ms·

Creusot helps you prove your Rust code is correct

66 points by fanf2 5mo ago

giltho 5mo ago
Fantastic work
rendaw 5mo ago
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)
- mbonnet 5mo ago
  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.
  - crackalamoo 5mo ago
    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?
    - phillc73 5mo ago
      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/ https://www.learntla.com/ [2] https://quint.sh/ https://quint.sh/ [3] https://apalache-mc.org/ https://apalache-mc.org/ [4] https://docs.rs/quint-connect/latest/quint_connect/ https://docs.rs/quint-connect/latest/quint_connect/
    - mbonnet 5mo ago
      it's generally another layer on top of things like unit testing, MC/DC coverage, etc. not all programs use formal verification though.
Trung0246 5mo ago
How does this differ from https://github.com/verus-lang/verus https://github.com/verus-lang/verus
- yjhjstz 5mo ago
  [flagged]
- isubasinghe 5mo ago
  Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html https://coma.paulpatault.fr/language/program.html). Verus encodes directly to SMT. Creusot may gain some more automation perhaps from this approach.
Loic 5mo ago
I like the name[0][1]. [0]: https://www.britannica.com/place/Le-Creusot https://www.britannica.com/place/Le-Creusot [1]: https://en.wikipedia.org/wiki/Le_Creusot https://en.wikipedia.org/wiki/Le_Creusot
deleted 5mo ago
[deleted]

66 points by fanf2 5mo ago

Fantastic work

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)

mbonnet 5mo ago
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.
- crackalamoo 5mo ago
  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?
  - phillc73 5mo ago
    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/ https://www.learntla.com/ [2] https://quint.sh/ https://quint.sh/ [3] https://apalache-mc.org/ https://apalache-mc.org/ [4] https://docs.rs/quint-connect/latest/quint_connect/ https://docs.rs/quint-connect/latest/quint_connect/
  - mbonnet 5mo ago
    it's generally another layer on top of things like unit testing, MC/DC coverage, etc. not all programs use formal verification though.

Trung0246 5mo ago

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

yjhjstz 5mo ago
[flagged]
isubasinghe 5mo ago
Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html https://coma.paulpatault.fr/language/program.html). Verus encodes directly to SMT. Creusot may gain some more automation perhaps from this approach.

Loic 5mo ago

I like the name[0][1]. [0]: https://www.britannica.com/place/Le-Creusot https://www.britannica.com/place/Le-Creusot [1]: https://en.wikipedia.org/wiki/Le_Creusot https://en.wikipedia.org/wiki/Le_Creusot

deleted 5mo ago

[deleted]