Verus: SMT-based verifier for Rust
==================================

Verus lets developers write specifications and proofs inside Rust and discharges them with an SMT solver, giving full functional correctness without a separate proof assistant.

Maintainer: CMU, Microsoft and community
Website: https://github.com/verus-lang/verus
Category: Verified implementations
Targets: Rust (systems and some cryptographic code)
Approach: Ghost specifications and SMT-discharged proofs in Rust itself
Access: Open source (MIT)
Status: Active
Strengths: Specs and code in one language. | High automation. | Active community.
Limits: SMT limits on nonlinear field arithmetic. | Requires writing Verus-flavoured Rust. | Less cryptographic precedent than hax.
Firms using it: none listed
Sources: https://github.com/verus-lang/verus

Source page: https://sorryfree.com/frameworks/verus/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13