Developing provably correct Rust code with Verus

Rust already does a lot of the hard work. It blocks many memory bugs, it makes out-of-bounds access stop the program instead of silently wandering off, and it gives teams a fast language with security benefits built in. But Amazon’s point is sharper: safer is not the same as proven correct. A program can still return the wrong answer, or leak something it was supposed to keep quiet about.

That is the gap Verus is meant to fill. Verus is an open-source verifier for Rust that checks code against a formal specification. A developer writes down what a function must do, in Rust-like annotations, and the tool tries to prove that the implementation satisfies those rules for every possible input. In the binary-search example, that means not just proving that a returned index stays in bounds, but also proving the harder negative case: if the function says there is no match, then the target really is not in the array.

The design choice matters. Verus keeps the specifications and proofs in the source file, so the work stays next to the code it describes. Rust compilers ignore those annotations, which means verified and unverified projects can still share the same code. And when something breaks, developers get Rust-style errors at the source level instead of being bounced into a separate proof language. That should make the whole thing less ceremonial and more usable.

Amazon says Verus already fits into its own Rust work, including key primitives for the Nitro Isolation Engine and other infrastructure. The company is also leaning on automation: Verus uses multiple solvers, often gives feedback in under a second, and can verify projects with thousands of lines of code. That speed matters for humans, and it matters for AI agents too, because fewer proof chores means more room to iterate.

The other interesting bit is what Verus does to Rust’s “unsafe” code. Rust lets developers drop out of the compiler’s safety net when they need performance, but Verus can still prove those sections safe. It also extends to concurrency, where locks can carry invariants and even the lock implementation itself can be proved. That’s the real pitch here: not trust the language, but prove the thing anyway.