Verus is a formal verification tool for the Rust programming language that uses SMT solvers in its implementation.
Verus has been used by Amazon Web Services and Microsoft for provably correct software development. The AutoVerus system uses large language models to construct Verus proofs for Rust programs.
References
External links