Verus: Verified Rust for low-level systems code
Verus: Verified Rust for low-level systems code
github.com GitHub - verus-lang/verus: Verified Rust for low-level systems code
Verified Rust for low-level systems code. Contribute to verus-lang/verus development by creating an account on GitHub.
Another, very similar verified superset of Rust is Creusot. I'm not sure what the benefits/downsides of each are besides syntax tbh.
This is also similar to Kani which also verifies Rust code. However, Kani is a model checker like TLC (the model checker for TLA+), while Verus and Creusot are SMT solvers like Dafny.
Interestingly, Verus (unlike both Kani and Creusot) has its language server, which is a fork of rust-analyzer (verus-analyzer).
1
comments
Wow, I really like their macro syntax! That seems very approachable to someone who usually doesn’t formally verify their code :)