Creusot helps you prove your Rust code is correct(github.com)

61 pointsby fanf25 hours ago5 comments

rendaw3 hours 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)
- mbonnet3 hours 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.
  - crackalamoo2 hours 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?
    phillc7336 minutes 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/
    [2] https://quint.sh/
    [3] https://apalache-mc.org/
    [4] https://docs.rs/quint-connect/latest/quint_connect/
Trung02463 hours ago
How does this differ from https://github.com/verus-lang/verus
- yjhjstzan hour ago
  [flagged]
Loic3 hours ago
I like the name[0][1].
[0]: https://www.britannica.com/place/Le-Creusot
[1]: https://en.wikipedia.org/wiki/Le_Creusot
3 hours ago
undefined
giltho4 hours ago
Fantastic work