Verus
A tool for formally verifying the correctness of Rust code using SMT-backed proofs.
Liked for integrating proofs directly into Rust code1234 in a programmer-friendly way that coding agents handle well.56 The most cited caveat is that it is still essentially a standalone language with its own syntax,7 and it is unclear how it handles proofs beyond what an SMT solver can do.8
Why people recommend it
Rust integration · 3
Commenters like how it embeds proofs into Rust code.
“I think they found a nice way to integrate proofs with the language.”
“integrates proof with macro in Rust”
Show 1 more
“extensions like Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look”
Works with LLMs · 2
Coding agents are reported to write Verus proofs well in Rust codebases.
“I have found that agents are good at writing Verus proofs in a Rust code base, and that these proofs have only a minimal negative effect on the normal compilation path.”
“I think they found a nice way to integrate proofs with the language.”
Programmer-friendly · 2
Seen as more approachable than other proof-of-correctness approaches.
“It's much more programmer-friendly than some other approaches.”
“it's genuinely amazing. I have been using it on my own Rust codebases for a while”
Low build impact · 2
Proofs add little cost to normal compilation and can run as a separate step.
“I have found that agents are good at writing Verus proofs in a Rust code base, and that these proofs have only a minimal negative effect on the normal compilation path.”
“Their tutorial seems ok”
Caveats and dissent
Custom syntax · 1
Described as essentially a standalone language with its own syntax and type system.
“Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem”
SMT limits · 1
It is unclear how it handles proofs beyond what an SMT solver can do.
“It's much more programmer-friendly than some other approaches.”
Unclear payoff · 1
It is hard to know when proofs are more productive than other techniques.
“I think they found a nice way to integrate proofs with the language.”
Learning resources · 1
The tutorial is called only okay, and Dafny or SPARK/Ada are suggested for fuller tutorials.
“Their tutorial seems ok”
Who recommends it in their own words
Threads where it came up
- Verus is a tool for verifying the correctness of code written in Rust 2 mentions
- LLMs are making formal software verification feasible at a much larger scale 1 mention
- What agents mean for Rust (and vice versa) 1 mention
- Bend – a language that blocks AI mistakes via proof and runs on GPUs 1 mention
- Developing provably correct Rust code with Verus 1 mention
- We have proof automation now 1 mention
Data: verus.json. Quotes are verbatim; the verdict and theme labels are written by a model from these comments, and every clause links to its sources.
All comments 8
“I think they found a nice way to integrate proofs with the language.”
“I have found that agents are good at writing Verus proofs in a Rust code base, and that these proofs have only a minimal negative effect on the normal compilation path.”
“integrates proof with macro in Rust”
“Their tutorial seems ok”
“Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem”
“extensions like Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look”
“It's much more programmer-friendly than some other approaches.”
“it's genuinely amazing. I have been using it on my own Rust codebases for a while”