Verus proves Rust code correct for every possible input
Developing provably correct Rust code with Verus
Amazon's Verus is an open-source automated program verifier for Rust that mechanically checks code against formal mathematical specifications for all inputs, catching corner cases that testing misses. Developers annotate source with Rust-like preconditions and postconditions, getting feedback in under a second, and AI agents can often handle proof generation. Verus also verifies unsafe blocks and concurrent code, restoring machine-checked safety guarantees for performance-critical work like AWS's Nitro Isolation Engine.
However, "more correct and secure" is not the same as "actually correct and secure".
- 63
If you found this interesting, you may also be interested to hear about some related projects with similar goals/scopes: Miri[0], Kani[1], and Creusot[2]. There looks to be some significant overlap between Verus, Kani, and Creusot but I've not used any of them so I'll refrain from trying to differentiate them.
[0]https://github.com/rust-lang/miri
- sourdecor
Verus seems to be exactly what I have been looking for! I discovered AllConcur[0] on HN a while back, and I wanted to port it to Go, but since it used TLA+ and C, and it was very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
I was talking to Gemini about comparing Verus to TLA+ and it said that TLA+ is usually used (for example) "to prove that a distributed consensus protocol is logically sound" but when I asked if Verus can do that too, it said yes. So Verus can be compiled and integrated with Rust, whereas TLA+ is used more for blueprint development that then guides the implementation in the mind of the implementer.
Seems awesome!
- nottorp
Would it help with the bugs in the new and improved ubuntu coreutils?
- Meneth
"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth.
- lukeify
Reminds me of Whiley, which was developed by one of my university professors.