Research topic

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 @ JBI

Binding constraintAlgorithms

A controller that ships its own stability proof, checked on the device in milliseconds, exists now. The route is what matters: obtain that certificate by checking boxes and it costs exponentially in joint count, obtain it from the structure of the mechanism and it costs nothing extra and works at any number of joints. What is left is expressing a task inside that structure, which is a modelling skill you can learn rather than a proof obstacle.

One of eight, and only one of them is physics. How we read a frontier →