Amazon researchers detail Verus, an automated verifier for Rust code

Verus is an open-source tool that mathematically verifies Rust programs against formal specifications, checking correctness across all possible inputs rather than sampling test cases. It builds on Rust's existing memory-safety guarantees to also confirm that code produces expected results and doesn't leak sensitive data.