Engineering boundary: the sub-50 ns sensor-to-actuator path is a target, not a measured silicon result. Timing-aware formal proofs, UltraScale+ timing closure, and hardware waveform equivalence remain open.
Sensor edge to guarded trigger
The present release connects kinematic models, diagnostics, scheduling, safety interlocks, and bit-true HDL paths without claiming the unfinished silicon timing result.
B-dot + AER
ADC normalisation, spike-rate quantisation, buffer decoding, and replay.
Moving frame
Doppler-Kuramoto synchronisation and UPDE remapping for pulsed FRC motion.
Merge window
Lifecycle scheduling, bank dynamics, safety checks, and Petri-net control.
Trigger fabric
Clocked debounced single-shot logic with a registerless fast-veto lane.
Evidence
Python/Verilator cosimulation, SymbiYosys safety/liveness proofs, and manifests.
Polyglot verification surface
◈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 — Safety and bookkeeping proofs for scheduling, capacitor dynamics, recovery, interlocks, and Petri nets.
◈Open formal flow — Yosys, SymbiYosys, z3, and Verilator establish bounded safety, liveness, and bit-true equivalence evidence.
◈Ecosystem boundaries — FUSION-owned physics kernels are detected through contracts, not silently reimplemented or dispatched locally.