Rust verification tools
This is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
We see static verification (formal verification) and dynamic verification (testing) as two parts of the same activity and so these tools can be used for either form of verification.
Dynamic verification using the proptest fuzzing/property testing library.
Static verification using the KLEE symbolic execution engine.
We aim to add other backends in the near future.
Tools and libraries
verification-annotationscrate: an FFI layer for creating symbolic values in KLEE
propverifycrate: an implementation of the proptest library for use with static verification tools.
scripts/cargo-verify: a tool for compiling a crate and either verifying main/tests or for fuzzing main/tests. (Use the
--backendflag to select which.)
compatibility-testtest crate: test programs that can be verified either using the original
proptestlibrary or using
propverify. Used to check that proptest and propverify are compatible with each other.
(Warning: these installation instructions are quite complicated, poorly tested and may be missing steps.)
Fuzz some examples with proptest
cd compatibility-test cargo test cd ..
(You can also use
./scripts/cargo-verify compatibility-test --backend=proptest --verbose.)
One test should fail – this is correct behaviour.
Verify some examples with propverify
./scripts/cargo-verify verification-annotations --tests
./scripts/cargo-verify compatibility-test --tests
No tests should fail.
Read the propverify intro for an example of fuzzing with
proptestand verifying with
Read the proptest book
Read the source code for the compatibility test suite.
(Many of these examples are taken from or based on examples in the proptest book.)
There is also some limited documentation of how this works.
- Overall installation instructions
Licensed under either of
- Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
propverify crate is heavily based on the design and API of the wonderful proptest property/fuzz-testing library. The implementation also borrows techniques, tricks and code from the implementation – you can learn a lot about how to write an embedded DSL from reading the proptest code.
proptest was influenced by the Rust port of QuickCheck and the Hypothesis fuzzing/property testing library for Python. (
proptest also acknowledges
regex_generate – but we have not yet implemented regex strategies for this library.)
This is not an officially supported Google product; this is an early release of a research project to enable experiments, feedback and contributions. It is probably not useful to use on real projects at this stage and it may change significantly in the future.
Our current goal is to make
propverify as compatible with
proptest as possible but we are not there yet. The most obvious features that are not even implemented are support for using regular expressions for string strategies, the
We would like the
propverify library and the
cargo-verify script to work with as many Rust verification tools as possible and we welcome pull requests to add support. We expect that this will require design/interface changes.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.
See the contribution instructions for further details.