Charon-based abstract interpretation pass on LLBC — the third DO-333 technique class

[avrabe]

Part of the V&V coverage initiative — Phase 5 (Abstract Interpretation). Long-term strategic investment; depends on rules_lean#1 landing first.

Context

Abstract interpretation is the missing third DO-333 technique class in PulseEngine's V&V chain. Alongside the hermetic Aeneas pipeline (tracked at rules_lean#1), Charon already exposes Rust MIR as LLBC — the same intermediate we are translating to Lean for theorem proving.

This issue is the strategic follow-up: build a modest abstract interpreter directly on LLBC, reusing the Charon toolchain and the Nix-hermetic build we are standing up for Aeneas. One Rust-MIR toolchain, analysis artefacts that live alongside the Lean / Rocq proofs, fits the same DO-330 tool-qualification story we are building.

Why on LLBC (not Rust MIR directly)

• Charon's LLBC is already the hermetic IR we commit to for Aeneas. Working on LLBC means one toolchain, one versioning story, one qualification dossier.
• LLBC preserves Rust semantics cleanly (moves, copies, borrows, reborrows) while simplifying compiler-specific details — good fit for AI lattices.
• MIRAI operates on Rust MIR directly; our prototype (see sigil#91, gale#23, rivet#191) will tell us what AI buys on our code. If the answer is "a lot," we invest here; if marginal, we document and pass.

Scope — first useful pass

A modest analyzer with three lattices:

• Interval — integer range analysis (catches overflow, underflow, OOB index)
• Sign — non-negativity and signedness tracking (catches division-by-zero, negative-length constructors)
• May-alias — conservative aliasing of references (catches borrow-related panics, mutable-reference use-after-move at the LLBC level)

Not in the first pass: shape analysis, relational domains, numerical abstractions beyond intervals. Keep it small and correct first; add precision later.

Acceptance

• Prerequisite: rules_lean#1 closed (hermetic Charon landing)
• New subsystem rules_lean/absint/ with:
  • Core lattice infrastructure in Rust or OCaml (Charon is OCaml; easier to share code)
  • Interval, sign, and may-alias lattices
  • Driver that consumes LLBC and emits an analysis report
• Bazel rule absint_check(name, llbc_srcs) analogous to aeneas_translate that runs the pass and fails on flagged violations (configurable)
• Documentation at rules_lean/docs/abstract-interpretation.md
• First end-to-end example on a small target crate (e.g. sigil varint or gale ring_buf), with the MIRAI prototype reports as baseline for comparison
• Traceability: analysis results link back to safety requirements via rivet

Rough effort

• Infrastructure + one lattice: ~1 month
• Three lattices + driver + Bazel rule: ~2–3 months total
• First useful end-to-end pass: ~3–4 months, paced against Aeneas landing

Why not Astrée

Astrée (AbsInt, commercial) has the industrial precedent (Airbus A380/A350 DAL A), but it only covers C and Ada, costs tens of thousands of EUR per year, and would drag in a separate toolchain PulseEngine does not otherwise need. It stays on the shelf for the C-shim boundary if a certification programme specifically requires it.

Why not MIRAI long-term

MIRAI is the prototype vehicle (see sibling issues sigil#91, gale#23, rivet#191). Research-grade, low recent activity, works on Rust MIR. If prototypes show strong signal, MIRAI could live alongside a Charon-based pass — but the strategic bet is the LLBC path because it integrates into the hermetic toolchain we are already building.

Related

• pulseengine/rules_lean#1 — Aeneas end-to-end pipeline (blocker)
• MIRAI prototypes: MIRAI prototype — evaluate abstract interpretation on crypto parser paths (varint + DSSE) sigil#91, MIRAI prototype — evaluate abstract interpretation on RTOS kernel primitives (ring_buf, scheduler, atomics) gale#23, MIRAI prototype — evaluate abstract interpretation on traceability engine internals (artifact store, link graph) rivet#191
• V&V coverage hub: rivet#184
• Reference: Charon paper (arXiv 2410.18042)