Provable by construction.
A controller isn't trustworthy because it passed testing — it's trustworthy because its stability is proven. This is the other half of Swap-2C, the companion to the energy receipt: where the receipt prices a decision, this certifies a controller. A closed-loop policy is checked against a Lyapunov function by interval branch-and-bound — a real proof over a whole region of the state space, not a grid of samples — which returns either a certified region of attraction or a concrete counterexample state. Near the equilibrium the certificate is analytic, where the linear term provably dominates; everywhere else it is proven box by box, with the enclosures inflated so the result is sound rather than merely sampled. The whole check runs on the device, in milliseconds — so a controller can carry its own proof to where it runs.
Tune the gains: the verifier proves V̇ < 0 by interval branch-and-bound and draws the certified region of attraction in gold — or finds the states where the pendulum's nonlinearity wins (red). Drop below kp ≈ g/L and the certificate correctly vanishes: the loop is unstable. Click the phase plane to release a trajectory.
In the field · learned Lyapunov certificates and certified training with branch-and-bound are the frontier of provable control (CT-BaB, FOSSIL). Swap-2C's line is its own: the certificate is cheap enough to run on the device, beside the joules receipt — a controller that ships both its cost and its proof.
↓ Whitepaper · PDFRead online◆ Living paperTechnical Report TR-2026-07 · Institute for Physical AI @ BMI