Verus is a tool for verifying the correctness of code written in Rust(verus-lang.github.io)
verus-lang.github.io
Verus is a tool for verifying the correctness of code written in Rust
https://verus-lang.github.io/verus/guide/
15 comments
> What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)
A trigger in SMT lingo is nothing of the sort. It’s simply an instruction to the solver about which instantiations of a universal quantifier should be considered, with the aim of getting a proof without too many specious steps.
The statement with the trigger on it is typically an assumption from e.g. a function specification. At some point the statement with the trigger may itself become a proof obligation elsewhere in the program, but that’s something that can be handled with SMT.
A trigger in SMT lingo is nothing of the sort. It’s simply an instruction to the solver about which instantiations of a universal quantifier should be considered, with the aim of getting a proof without too many specious steps.
The statement with the trigger on it is typically an assumption from e.g. a function specification. At some point the statement with the trigger may itself become a proof obligation elsewhere in the program, but that’s something that can be handled with SMT.
[deleted]
I tried it not long ago - it's really cool just a tad sad that the rust eco-system didn't allow verus to be more streamlined in the tool and requires these little shenanigans with a different build of it - it felt a bit clunky to swap cargo for the verus one ; but the tool is definitely needed right now
Do you have any reference to the Rust community “not allowing” something? This seems more like a case of a relatively niche tool doing what it needed to do to work, but not (yet) some broader effort to upstream or integrate this into cargo or rustup. I couldn’t find any RFCs or anything, for instance.
I didn’t read OP as saying “the community won’t allow” but more “the tooling doesn’t allow” for what they want to do.
[deleted]
So far out of what I've looked at, Kani blends into the Rust language best. Verified code snippets look a lot like unit tests.
Verus wraps everything in its macro that makes rust-analyzer etc unhappy.
#[kani::proof]
fn check_my_property() {
// Create a nondeterministic input
let input: u8 = kani::any();
// Call the function under verification
let output = function_under_test(input);
// Check that it meets the specification
assert!(meets_specification(input, output));
}
Verus wraps everything in its macro that makes rust-analyzer etc unhappy.
I just attended a talk at Northeastern (Boston) on Verus, it's genuinely amazing. I have been using it on my own Rust codebases for a while, and it has made me think deeper about the structure and semantics of Rust code.
Oh hey I worked on this :)
I wonder whether this could be used as an additional guardrail for LLM coding
[deleted]
Clippy with unstable features enabled catches most if not all of these cases automatically? This seems like it needs more work to do the same thing clippy does.
I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.
I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.
I have written complex proofs for distributed system using verus which are certainly not expressed by clippy
It's not clear what they do when they need to prove something beyond what an SMT solver can do. That's supposed to be covered in section 11.4, "forall and exists: writing and using triggers, inline functions". What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)
That's the right approach - use an SMT solver for the easy stuff, which should be 90-95% of the proofs. Then use something else for the hard stuff. We used the Boyer-Moore prover, a predecessor to the ACL system. Others have used proof-checkers, and Lean. There's recent interest in using LLMs to drive something like Lean; the LLMs make mistakes but the proof checker catches them. Looks like they haven't gotten to this part yet.
The way to partition the problem is to use two "assert" statements in succession. An assert statement is a proof goal before the assert, and is assumed true after the assert. So when you hit something hard, you try to bracket it with
and get everything to verify with the SAT solver except
Now you have a self-contained expression to prove by some external means. Often you can prove such statements in a generic form, and reuse the proofs.
There should be object invariants, except that Rust doesn't have objects. It does have structs with associated functions and encapsulation. You need some way to express that structs with internal state are consistent before and after being called. C++ has about the right amount of hiding ("abstraction") for this, with public and private fields and functions for objects. Rust's idea of "private" means "same module", not "same struct". So invariants would apply to a module. Then you have to be very organized about when control enters and leaves the module. Like not calling pub functions from inside the module, because the module invariants may not be valid at internal entry to a pub function.
The extensional equality thing is interesting. It needs more description. The basic problem is this: for some types, such as sets, hash tables, and such, objects are supposed to be considered equal if you can't tell from the outside that they're different internally. Formally, the type must have the property
That has to be proven for all functions which accept T. Then you can treat type values as equal even if their internal representation is different. Such types can't have any access functions or pub variables which allow you to examine the internal state. For example, if you convert a set to a vector, it has to be sorted, so that you can't tell what the internal order was.
Nice work. Keep plugging.
[1] https://animats.com/papers/verifier/verifiermanual.pdf