Verification lanes
◈Python + Rust — Reference models and native hot paths with explicit fallback and cross-runtime contracts.
◈SystemVerilog — Synthesizable B-dot quantisation, trigger, and zero-cycle veto logic with self-checking traces.
◈Julia + Go — Independent scientific lanes and DAQ replay, kept in parity with public contracts where applicable.
◈Lean — Two-tier formal: Lean proves software invariants for scheduling, capacitor dynamics, recovery, interlocks, and Petri nets.
◈SymbiYosys — The hardware tier proves safety and liveness properties of the RTL trigger and veto logic.
◈Open formal flow — Yosys, SymbiYosys, z3, and Verilator establish bounded safety, liveness, and bit-true equivalence evidence.
Fault-injection cosimulation
MIF-015 stress-propagation cosimulation drives a B-dot ADC stream degraded by MIF-017 through the MIF-007 quantiser into the MIF-008 trigger fabric, asserting no fire under veto, one shot per continuous arm, and no hold-counter underflow through the Verilator RTL under realistic sensor faults.