engineering 3 posts

← all posts · monogate.org

We Injected a Fault and the Safety Proof Held

A saturating guard keeps a plant's state inside a safe envelope for all time, for any controller, under any bounded disturbance. We proved it in Lean (sorryAx-free), turned the proof into a number — and then made that number a machine-checked theorem too — and measured it holding on a real FPGA, on a noisy breadboard, and on a genuinely nonlinear plant, while we injected an actuator fault on purpose. The breadboard limit-cycled and looked nothing like the simulation; the envelope held anyway, because safety rides on the saturation, not on good control. Here is the receipt, the one place a skeptic would push, and exactly what we do not claim.

engineering

We Put the Proof on a Real FPGA

One verified math source compiles to software, RTL, and a GPU shader. We stopped trusting the model and ran each artifact for real — C on gcc, RTL in Verilator, a shader on an NVIDIA GPU, and the datapath on an Arty A7 FPGA — checking every output against a Lean-proved error bound. Each one held. Building it found six real bugs. Here is the receipt, and here is exactly where it doesn't hold.

engineering

What BEST Routing Saves

Node-count and wall-clock benchmarks across 8 elementary functions. BEST dispatch vs naive EML.

engineering