Rustproof is a compiler plugin for the Rust programming language. It generates verification conditions for functions with supplied preconditions(P) and postconditions(Q). That is, given a supplied postcondition on a function, rustproof uses predicate transformer semantics to generate a weakest precondition(WP(S, Q)) from the postcondition and a body of statements(S). The verification condition P->WP(S,Q) is then checked for validity by a SMT solver (z3). This process results in a proof of function correctness.

• rustc 1.12.0-nightly (2016-08-12).

• z3

Your installation of z3 needs to be in your PATH for rustproof to work.

• Integer arithmetic
  • isize and usize are unsupported
• Boolean expressions, variables, and literals
• Assertions (integer/boolean)
  • assert_eq!() is unsupported
• If statements

Add rustproof as a dependency in Cargo.toml

[dependencies]
rustproof = { git = "https://github.com/Rust-Proof/rustproof.git" }

#![plugin(rustproof)] is required in each file where rustproof is used. Typically this is placed at the beginning of a file.

Rustproof uses a custom attribute condition to allow declaring pre/postconditions on functions.

The attribute is supplied as: #[condition(pre=" ", post=" ")] and must be supplied before a function definition.

See USAGE for a detailed explanation of the attribute system.

See EXAMPLES for example functions with condition attributes.

Additionally, #![plugin(rustproof(debug))] prints out basic blocks of each function annotated with #[condition(..)], as well as a step-by-step view of generating the verification condition.

Matthew Slocum
Sami Sahli
Vincent Schuster
Michael Salter
Bradley Rasmussen
Drew Gohman
Matthew O'Brien

Please report all issues on the github issue tracker.

Rustproof is distributed under the terms of both the MIT license and the Apache License (Version 2.0).

See LICENSE-APACHE, LICENSE-MIT, and COPYRIGHT for details.