Module audit 

Audit trail generator — traceability chain.

Traces the full chain from paper reference → equation → proof obligation → falsification test → Kani harness. Detects orphaned obligations and untested equations.

Structs

AuditReport

Audit result summarizing traceability coverage.

BindingAuditReport

Binding audit result — cross-references contracts with implementations.

Functions

audit_binding

Audit the binding registry against a set of contracts.

audit_contract

Run a traceability audit on a contract.