Chapter 8.1. Design Principles and Verification Modes

8.1.1 Design Principles

The verification is grounded on three assumptions:

  • Origin of Unsafe Code: All instances of undefined behavior arise from unsafe code — safe Rust's type system already rules out data races, use-after-free, null-pointer dereferences, and buffer overflows. Verification focuses exclusively on the unsafe boundary where the compiler's guarantees end.
  • Explicit Safety Properties: Safety properties of unsafe code are documented through attributes:
    • #[rapx::requires(...)] on unsafe functions — preconditions callers must satisfy before invoking the function.
    • #[rapx::invariant(...)] on structs — structural invariants that must hold for every instance.
    • #[rapx::ensures(...)] on unsafe trait methods — postconditions that every implementor of the trait must guarantee. Only unsafe trait implementations involve #[rapx::ensures]; regular functions use #[rapx::requires] instead. See the Rust Safety Standard for the underlying methodology. Each annotation declares a contract, making safety obligations machine-checkable rather than implicit in documentation comments. The full contract syntax is described in Chapter 8.3.
  • Soundness of Unsafe Code Usage: Unsafe code is considered safe if every possible execution path satisfies the safety properties of every unsafe callee it invokes. If a path exists that would violate even one property, the call site is flagged as unproved.

8.1.2 Verification Modes

RAPx supports three verification modes, selectable via cargo rapx verify --mode <MODE>. Each mode targets a different use case in the development workflow.

scan Mode (Default)

Fully automatic. The VerifyTargetCollector (target.rs) walks all function bodies in the crate using a HIR visitor. It selects functions for verification if:

  • the function body contains an unsafe { } block, or
  • the function is a method on a struct with #[rapx::invariant] annotations.

For each selected function, build_function_target collects all unsafe call sites from the MIR body and resolves each callee's safety contracts from #[rapx::requires] annotations or a bundled JSON database for standard library functions (see Chapter 8.3).

cargo rapx verify --mode scan

targeted Mode

Only verifies functions explicitly annotated with #[rapx::verify]. No pre-filter is applied; the collector simply checks for the attribute presence.

cargo rapx verify --mode targeted

The annotation pattern:

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]

fn main() {
#[rapx::verify]
#[rapx::requires(ValidPtr(self.0, T, 1))]
unsafe fn my_function(ptr: *mut u32, len: usize) {
    unsafe { ptr::write(ptr.add(len - 1), 0); }
}
}

Verifying the standard library. When the crate under analysis relies on the #[cfg_attr(rapx, ...)] pattern (as the annotated rust-std fork does), the rapx cfg and the tool registration must be injected through RUSTFLAGS:

export RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)"
cargo rapx verify --module slice --mode targeted

Without --cfg=rapx the cfg_attr-gated markers never expand, and the verifier reports that the module matched no functions.

invless Mode

For structs that lack #[rapx::invariant] annotations, their safety contracts are still verifiable through constructor-to-caller method chains. invless mode enumerates all paths from each constructor through zero or more &mut self mutators to a final reader method. For each chain, it collects the constructor's #[rapx::requires] contracts (if any), filters out properties invalidated by subsequent field mutations, merges in the reader method's own #[rapx::requires], and verifies that the accumulated contracts entail the callee's safety requirements at every unsafe call site along the path. If every constructor → mutator* → method chain passes for a given struct, the struct's usage is considered sound.

cargo rapx verify --mode invless

8.1.3 Common Options

--prepare-targets lists all verification targets and their resolved contracts without running verification (see Chapter 8.2 for detailed examples).

The --crate <CRATE> and --module <PATH> flags restrict verification to a specific crate and module. When combined, only functions in the intersection are verified. This is commonly used for verifying standard library modules:

cargo rapx verify --crate core --module slice

The crate prefix is matched flexibly, so --module slice matches core::slice::*.

The --postfix-repeat flag provides manual control over loop unrolling depth. By default (auto), the verifier chooses the repeat count automatically. When auto-detection produces inaccurate results, --postfix-repeat=N disables auto-expansion and fixes the repeat count to N. The full mechanism is described in Chapter 8.4.1 Path Extraction.

The --debug-contracts flag prints the full contract resolution for every verification target: each unsafe callee with its resolved contracts, and the caller's own contracts in expanded form. Useful for diagnosing missing or unexpected contract resolutions:

cargo rapx verify --debug-contracts