MIRAI prototype — evaluate abstract interpretation on crypto parser paths (varint + DSSE)

[avrabe]

Part of the V&V coverage initiative — Phase 5 (Abstract Interpretation).

Context

Abstract interpretation is the one layer of the PulseEngine V&V chain we do not yet run — the third DO-333 technique class alongside theorem proving (Rocq / Lean) and bounded model checking (Kani). Before committing to a long-term investment, we are running three weekend-scale prototypes across sigil, gale, and rivet to understand what property classes AI catches on our actual code, and whether the signal is worth the integration cost.

sigil is the first prototype target: pure Rust, minimal unsafe, integer-heavy parser code, and already has Verus + Kani + Lean baselines we can compare against. This matches the SymCrypt/Aeneas precedent (crypto in Rust verified multiple ways).

Tool

MIRAI — abstract interpreter for Rust MIR from Meta. Research-grade, low recent activity but open-source. Designed for Rust specifically; covers integer overflow, panic reachability, and some memory properties.

Target code paths

• src/lib/src/wasm_module/varint.rs — varint decoder (integer arithmetic, overflow edges)
• DSSE envelope parser — length bounds, malformed-input handling
• Ed25519 entry surface — signature length checks, format validation

Property classes to watch for: integer overflow in signature offsets, out-of-bounds byte-slice reads, division/modulo edge cases, panic-freedom on adversarial input.

Acceptance

• MIRAI installed hermetically (ideally via Nix or pinned binary) and running on sigil's parser code paths
• Report committed at docs/verification/mirai-prototype-report.md documenting:
  • Which code paths were analyzed and how
  • What properties MIRAI flagged (true positives, false positives)
  • Side-by-side comparison with existing Verus annotations (verus_proofs/) and Kani harnesses — overlap vs distinct findings
  • Integration cost assessment (toolchain, CI time, maintenance)
  • Verdict: is the signal worth the integration cost?
  • Go / no-go recommendation for adopting MIRAI as a regular CI gate on sigil
• Findings summary posted back to the V&V hub (rivet#184) under Phase 5

Related

• Sibling prototypes (parallel experiments): pulseengine/gale, pulseengine/rivet (to be filed)
• Long-term follow-up: pulseengine/rules_lean — Charon-based value analysis pass on LLBC (to be filed, blocked on rules_lean#1)
• V&V coverage hub: rivet#184

Non-goals

• Production adoption. This is an evaluation, not a commitment. If MIRAI does not earn its keep, we document that and move on.
• Replacing Verus / Kani. Abstract interpretation is complementary, not substitutive.