ravencheck

ravencheck is a tool for symbolic verification of Rust code, using guaranteed-decidable SMT queries for predictable results.

Usage

First, make sure you have the CVC5 SMT solver available. You should be able to run cvc5 --version in your dev environment.

Then, to use ravencheck, add its GitHub repository as a dependency in your Cargo.toml file:

# Cargo.toml
...
[dependencies]
ravencheck = { git = "https://github.com/cuplv/ravencheck" }
...

Alternatively, you can clone the repo and use its path on your filesystem as the dependency:

# Cargo.toml
...
[dependencies]
ravencheck = { path = "path/to/cloned/repo" }
...

You will then use the #[ravencheck::check_module] macro on modules in which you want to use verification. See examples/sets.rs for an example.

About

"Raven" is an acronym for relationally-abstracted verification encoding, the technique that is used to reduce verification conditions to a decidable fragment of first-order logic (specifically, the Extended EPR fragment).