Verification of Distributed System using Verus

Verus is an open-source tool for formally verifying Rust programs. You write your executable Rust code alongside specifications (preconditions, postconditions, invariants) and optional proof code, and Verus uses automated SMT solvers to prove that the code satisfies those specs for all executions, without adding runtime checks.

It is aimed at verifying low-level systems code, leveraging Rust’s ownership and borrowing model to make reasoning about memory safety and aliasing more tractable.