Modules§
- audit
- book
- certify
pv certify— produce a whole-model proof certificate.- check_
parity pv check-parity— SEMANTIC gate for parity-matrix contracts.- codegen
pv codegen— generate Rustdebug_assert!() from YAML contracts.- coq
- coverage
- diff
- equations
- explain
- extract
pv extract-pytorch— extract kernels fromPyTorchsource.- flux
- fuzz
- generate
- graph
- infer
- invariants
- kaizen
pv kaizen— fleet-wide contract enforcement improvement.- kani
- lean
- lean_
status - lint
- migrate
- mirai
- pipeline
- probar
- proof_
status - query
pv query— Search contracts by intent, regex, or literal match.- roofline
- scaffold
- score
pv score— Quantitative contract and codebase scoring.- status
- tla
- unlock
- validate
- verify_
bindings - Verify that functions named in binding.yaml exist in crate source.
- verify_
pipeline pv verify-pipeline— compositional shape verification across contracts.- verify_
structure pv verify-structure— verify model architecture matches contracts.