Formal verification strategy (Kani + Verus + Rocq)

[avrabe]

Context

Rivet is a safety-critical traceability tool. Its validation engine must be provably correct — if it says PASS, all rules are actually satisfied. For ISO 26262 tool qualification (TCL 1), formal correctness evidence is the strongest argument.

The project already has proptest (property-based testing), cargo-fuzz (fuzzing), and Miri (UB detection). This issue adds three layers of formal verification on top.

Design: Verification Pyramid

Layer 1: Kani (bounded model checking)

Proves absence of panics, overflows, and unreachable states. ~10-15 harnesses for:

• LinkGraph::build() — no panics for any valid store+schema
• parse_artifact_ref() — all inputs parse or return clean error
• Schema::merge() — merge never panics, preserves all types
• validate() cardinality logic — exhaustive case coverage
• detect_circular_deps() — DFS terminates, finds all cycles
• MODULE.bazel parser — all byte inputs produce CST or diagnostics

Layer 2: Verus (functional correctness)

Proves validation is sound and complete:

• Soundness: PASS → all traceability rules satisfied
• Completeness: rule violated → diagnostic emitted
• Backlink symmetry: forward link ↔ backlink always holds
• Conditional rule consistency: non-contradictory when co-firing
• Reachability correctness: transitive closure is exact

Layer 3: Rocq / coq-of-rust (metamodel proofs)

Proves schema semantics are well-defined:

• Schema satisfiability: rules aren't contradictory
• Monotonicity: adding artifacts doesn't invalidate existing valid ones
• Link graph well-foundedness: validation terminates
• ASPICE V-model completeness: schema enforces full chain

Rivet artifacts

• REQ-030
• DD-025, DD-026, DD-027
• FEAT-049, FEAT-050, FEAT-051

References

• Kani: https://github.com/model-checking/kani
• Verus: https://github.com/verus-lang/verus
• coq-of-rust: https://github.com/formal-land/coq-of-rust
• ISO 26262 Part 8: Tool qualification