Module verify 

The staged verification pipeline.

Contract-based, path-sensitive verification of safety properties: collect targets and contracts, extract SCC-aware paths, slice them backward, execute the relevant MIR symbolically, and discharge each property with Z3.

Modules

api_classify 🔒

Standard-library API call classification helpers.

call_summary 🔒

Interprocedural call summaries for the staged verifier.

contract 🔒

Contract parsing, resolution, and rendering.

def_use 🔒

Verify-specific extensions for def-use computation.

display 🔒

Rendering of contracts, function signatures, and verification results.

driver 🔒

Driver utilities for the staged verifier pipeline.

engine 🔒

Symbolic-VM-based verification engine.

loop_sensitivity 🔒

Loop-sensitivity planning for the staged verifier.

path_extractor 🔒

Path extraction for verification targets.

property_checker 🔒

Unified property checker for the symbolic VM.

report 🔒

Diagnostics and summaries for the staged verifier pipeline.

slicer 🔒

Backward data-dependency slicer.

target 🔒

Discovery of verification targets and their contract obligations.

type_invariants 🔒

Standard-library type-invariant generation.

vm 🔒

Symbolic MIR Virtual Machine.