Verified controller zoo — Monogate Forge

One source → every target — proved, simulated, and (where it exists) measured.

Each card below was produced by one command (make all) from a single EML source. From that one source Forge emits every target it can — general-purpose software, GPU shaders, LLVM IR, machine-checked proofs (Lean / Coq / Isabelle), safety-critical (Ada / SPARK, AUTOSAR, AADL, ROS2), a smart contract, a zk circuit, and — for the RC filter, which is an actual circuit — a SPICE netlist, a KiCad schematic, and a JLCPCB fab bundle. Alongside the code sits a contract proof whose axiom footprint is clean of sorryAx, a simulation whose measured quantity satisfies the proved bound, and links to the raw evidence. This page is a generated view of that evidence — nothing is hand-authored; a proof that weren't clean, or a sim check that didn't hold, would show in red. (FPGA RTL — Verilog/VHDL/Chisel — is honestly absent: it needs an @target(fpga) clock annotation these scalar sources don't carry. The tool skips what it can't emit rather than fake it.)

Reproduction tiers: LOCAL one command, no heavy toolchain · TOOLCHAIN re-derive with Lean / Vivado · REPLAY captured on real hardware, replayed from evidence. 5 controllers + 2 theorems · 151 target emissions · 4 with real-hardware evidence.

Aerospace actuator band guard (FPGA — Arty A7)

examples/actuator_guard.eml · sha256 adaa434e2a58679c

32 targets from one source

softwareccppcsharpgdscriptgojavajavascriptkotlinluaumatlabpythonrustswiftwasm

gpu shaderglslglsl-eshlslmetalwgsl

fpga rtlchiselverilogvhdl

compiler IRllvm

proofcoqisabellelean

safety-criticalaadlada/sparkautosarros2

blockchainsolidityzkproof

proof ✓ cleansim ✓ holdshardware replay

proof footprint re-derived 2026-07-02T04:37:24Z from the emitted Lean (not a hand-written probe) · axiom trail

sim plot

The same claim, three ways. The theorem actuator_command_within_band proves the guarded actuator command is always within the certified flight-envelope band [u_min, u_max], for any controller inputs; the sim shows 0 = 0 (the raw command peaks at ±4.53 (well past the band) yet the guarded output never leaves [-1.0,1.0] — the clamp the theorem proves and the RTL/silicon runs); and the same behavior was measured on real hardware.

report evidence.json axiom trail c wgsl verilog lean solidity

Saturating clamp (output bounded to [-1, 1])

examples/clamp_bounded.eml · sha256 602c87f60a2a9b9b

29 targets from one source

softwareccppcsharpgdscriptgojavajavascriptkotlinluaumatlabpythonrustswiftwasm

gpu shaderglslglsl-eshlslmetalwgsl

compiler IRllvm

proofcoqisabellelean

safety-criticalaadlada/sparkautosarros2

blockchainsolidityzkproof

proof ✓ cleansim ✓ holds

proof footprint re-derived 2026-07-02T04:37:24Z from the emitted Lean (not a hand-written probe) · axiom trail

sim plot

The same claim, two ways. The theorem clamp_in_unit_interval proves clamp_unit(x) is always within [-1, 1] for every input x; the sim shows 1.0 ≤ 1.0 (clamp band [-1.0, 1.0]).

report evidence.json axiom trail c wgsl lean solidity

Iterated-exponential Khovanskii finiteness (depth 2)

machlib · MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional

a machine-checked result — a proof, not a codegen kernel

proof ✓ cleansim ✓ holds

proof footprint re-derived 2026-07-02T04:37:24Z from the machlib module · axiom trail

sim plot

The same claim, two ways. The theorem MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional proves a polynomial in the tower (x, eˣ, e^{eˣ}) that is nonzero at even one interior point has only FINITELY many zeros on (a,b) — the count derived from Rolle's theorem, not cited from Khovanskii; the sim shows 3 = 3 (count stable under 100× grid refinement ⇒ finite; e^(e^x) never vanishes so adds no zeros — consistent with the machine-checked bound).

Depth-2 shown here (proof + zero-count witness). Depth-3 is ALSO proven clean (MachLib.IterExpDepth3Bound.chain3_khovanskii_bound_unconditional); the ∀N generalization is in progress (lemma-1 + the reduce seam are done, machine-checked). General-depth PfaffianFunction.zero_bound STILL cites the classical Khovanskii axiom — only depths 1–3 are counted, not quoted.

report evidence.json axiom trail sim data

PID controller (output clamped to actuator range)

examples/pid_controller.eml · sha256 4d51cd9248714388

29 targets from one source

softwareccppcsharpgdscriptgojavajavascriptkotlinluaumatlabpythonrustswiftwasm

gpu shaderglslglsl-eshlslmetalwgsl

compiler IRllvm

proofcoqisabellelean

safety-criticalaadlada/sparkautosarros2

blockchainsolidityzkproof

proof ✓ cleansim ✓ holdshardware replay

proof footprint re-derived 2026-07-02T04:37:24Z from the emitted Lean (not a hand-written probe) · axiom trail

sim plot

The same claim, three ways. The theorem pid_output_clamped proves the control output is always within the actuator band [OUT_MIN, OUT_MAX] = [-1, 1]; the sim shows 1.0 ≤ 1.0 (actuator band [-1.0, 1.0]); and the same behavior was measured on real hardware.

report evidence.json axiom trail c wgsl lean solidity

RC low-pass filter (τ = R·C, step response)

examples/rc_filter.eml · sha256 ed5acb7a4025d3f1

32 targets from one source

softwareccppcsharpgdscriptgojavajavascriptkotlinluaumatlabpythonrustswiftwasm

gpu shaderglslglsl-eshlslmetalwgsl

compiler IRllvm

proofcoqisabellelean

safety-criticalaadlada/sparkautosarros2

blockchainsolidityzkproof

circuit/fabjlcpcbkicadspice

proof ✓ cleansim ✓ holdshardware replay

proof footprint re-derived 2026-07-02T04:37:24Z from the emitted Lean (not a hand-written probe) · axiom trail

sim plot

The same claim, three ways. The theorem rc_time_constant_def proves the filter time constant is exactly τ = R·C; the sim shows 0.0068 ≤ 0.01 (settles to Vin within 5τ); and the same behavior was measured on real hardware.

report evidence.json axiom trail c wgsl lean solidity spice

Closed-loop safety envelope under an injected fault

machlib · MachLib.Real.first_order_clamp_envelope

a machine-checked result — a proof, not a codegen kernel

proof ✓ cleansim ✓ holdshardware replay

proof footprint re-derived 2026-07-02T04:37:24Z from the machlib module · axiom trail

sim plot

The same claim, three ways. The theorem MachLib.Real.first_order_clamp_envelope proves for a first-order plant with a saturating actuator clamp (|u|≤U) and bounded disturbance (|w|≤W), the state stays within the envelope X=(U+W)/(1−a) for ALL time and ANY controller; the sim shows 0.8 ≤ 2.0 (state stays inside the proved envelope X*=(U+W)/(1−|a|) even after the injected fault — safety rides on the clamp, not on good control); and the same behavior was measured on real hardware.

The envelope is a conservative worst-case SAFETY bound — real trajectories sit well inside it (here the fault peak is ~40% of the envelope). That margin IS the safety, not a defect: the bound rests on the actuator clamp, not on good control. Measured on real hardware (ESP32 RC + a nonlinear diode-RC plant) it held under an injected fault while the breadboard limit-cycled.

report evidence.json axiom trail sim data

Bounded sine oscillator (|output| ≤ amplitude)

examples/sine_oscillator.eml · sha256 73837d61bea80a15

29 targets from one source

softwareccppcsharpgdscriptgojavajavascriptkotlinluaumatlabpythonrustswiftwasm

gpu shaderglslglsl-eshlslmetalwgsl

compiler IRllvm

proofcoqisabellelean

safety-criticalaadlada/sparkautosarros2

blockchainsolidityzkproof

proof ✓ cleansim ✓ holds

proof footprint re-derived 2026-07-02T04:37:24Z from the emitted Lean (not a hand-written probe) · axiom trail

sim plot

The same claim, two ways. The theorem sine_oscillator_amplitude_bound proves |A·sin(ωt)| ≤ A for A ∈ [0,1], ω ∈ [0, 1e4], t ≥ 0; the sim shows 0.8 ≤ 0.8 (amplitude bound |·| ≤ 0.8).

report evidence.json axiom trail c wgsl lean solidity