How can I check AI-written Rust beyond unit tests?

Use Sail with Verus for Rust that needs stronger checks than unit tests. Verus checks implementations against written contracts, such as preconditions, postconditions and invariants. Sail makes repeated verification faster and gives coding agents access to it through MCP.

Start with sail new --lib demo to create a Verus project, or use sail verify in an existing one. An agent can write code, contracts and proofs, then verify and check repairs through Sail. Cached Z3 answers and unchanged proofs are reused between attempts.