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 (Lean / Rocq) and bounded model checking (Kani). We are running three weekend-scale prototypes across sigil, gale, and rivet to understand what property classes AI catches on our actual code before committing to a long-term investment.
rivet is the third prototype target. Different from the other two: this is not primitives or crypto — it is a traceability engine with artifact indexing, link graph analysis, and YAML parsing. The question is whether MIRAI catches different property classes in higher-level data-structure code than it does in the kernel / crypto targets.
Tool
MIRAI — abstract interpreter for Rust MIR from Meta. Research-grade, low recent activity, open source. Designed for Rust; covers integer overflow, panic reachability, some memory properties.
Target code paths
rivet-core/src/store.rs — artifact storage / retrieval, index lookupsrivet-core/src/proofs.rs — Kani-harnessed paths (compare MIRAI and Kani findings head-to-head)- Link graph analysis — coverage computation, reachability queries
- Schema validation — YAML field access, required-field checks
Property classes to watch for: out-of-bounds on artifact-index access, integer overflow in counts, panic-freedom on malformed YAML, unreachable-code paths in validation.
Acceptance
Cross-repo synthesis
After all three prototypes (sigil, gale, rivet) complete, we want a cross-repo summary: does MIRAI behave consistently across code styles (crypto parsers, kernel primitives, data-structure code)? That synthesis belongs in the V&V hub update, not in any single prototype report.
Related
- Sibling prototypes (parallel experiments): pulseengine/sigil, pulseengine/gale
- Long-term follow-up: pulseengine/rules_lean — Charon-based value analysis pass on LLBC
- V&V coverage hub: rivet#184
Non-goals
- Production adoption. Evaluation only.
- Replacing Kani. Abstract interpretation is complementary, expected to catch classes Kani does not (non-terminating analysis, cross-function integer-range invariants).
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 (Lean / Rocq) and bounded model checking (Kani). We are running three weekend-scale prototypes across sigil, gale, and rivet to understand what property classes AI catches on our actual code before committing to a long-term investment.
rivet is the third prototype target. Different from the other two: this is not primitives or crypto — it is a traceability engine with artifact indexing, link graph analysis, and YAML parsing. The question is whether MIRAI catches different property classes in higher-level data-structure code than it does in the kernel / crypto targets.
Tool
MIRAI — abstract interpreter for Rust MIR from Meta. Research-grade, low recent activity, open source. Designed for Rust; covers integer overflow, panic reachability, some memory properties.
Target code paths
rivet-core/src/store.rs— artifact storage / retrieval, index lookupsrivet-core/src/proofs.rs— Kani-harnessed paths (compare MIRAI and Kani findings head-to-head)Property classes to watch for: out-of-bounds on artifact-index access, integer overflow in counts, panic-freedom on malformed YAML, unreachable-code paths in validation.
Acceptance
docs/research/mirai-prototype-report.mddocumenting:rivet-core/src/proofs.rs— did MIRAI find anything Kani missed, or vice versa?Cross-repo synthesis
After all three prototypes (sigil, gale, rivet) complete, we want a cross-repo summary: does MIRAI behave consistently across code styles (crypto parsers, kernel primitives, data-structure code)? That synthesis belongs in the V&V hub update, not in any single prototype report.
Related
Non-goals