rapx/verify/mod.rs
1//! The staged verification pipeline.
2//!
3//! Contract-based, path-sensitive verification of safety properties: collect
4//! targets and contracts, extract SCC-aware paths, slice them backward, execute
5//! the relevant MIR symbolically, and discharge each property with Z3.
6
7pub(crate) mod api_classify;
8pub(crate) mod call_summary;
9pub(crate) mod contract;
10pub(crate) mod def_use;
11pub(crate) mod display;
12pub(crate) mod driver;
13pub(crate) mod engine;
14pub(crate) mod loop_sensitivity;
15pub(crate) mod path_extractor;
16
17pub(crate) mod property_checker;
18pub(crate) mod report;
19pub(crate) mod slicer;
20pub(crate) mod target;
21pub(crate) mod type_invariants;
22
23pub(crate) mod vm;