Position & nano-scale demonstration
Energy Is the Certificate
The unclaimed intersection in Physical AI: one scalar energy that is both what an agent minimizes to act and what verifies that action before it commits.
Charlot Lab, Institute for Physical AI @ BMI
1 · The field predicts, then acts
The dominant architecture of 2025–26 Physical AI is control-first by construction. In most deployed systems the world model is a service consumed by a separately-optimized decider: Cosmos-Predict feeds a separate policy; a generalist VLA generates a goal image a separate action expert executes; World-Gym uses a learned model as a post-hoc scoring oracle judged by a VLM.1,2 The caveat, which we make explicit because a hostile reviewer will: this bolt-on pattern is no longer universal. WorldVLA and related work fuse prediction and action in one transformer, and π\*0.6/RECAP shows continuous on-robot reinforcement learning at the flagship.3,4 Continuous interaction is becoming standard; it is not what this work claims.
What every one of these systems shares is the commitment rule. A plan is chosen because it scores well under the model — lowest predicted cost, highest predicted reward, best VLM verdict. That is an expected-value filter, and even the safety-aware members of the family (SafeDreamer plans safety inside imagination; Cosmos-Policy samples many rollouts and keeps the best) supply a statistical gate, not a formal one.5 No system carries a worst-case certificate — a contraction or bound-propagation condition — that must hold before the action commits. Genie 3's own documentation reports coherence drift after minutes;6 that is the empirical fingerprint of having no scalar whose violation signals left the physical manifold.
2 · The empty intersection
Four recent lines of work each occupy one edge of the claim we make, and each stops one edge short.
Energy as the learning target. EBT-Policy replaces a diffusion policy's ~100-step denoiser with energy-equilibrium seeking in a handful of steps and shows unexplained zero-shot failure recovery.7 ECD formulates long-horizon planning as the minimizer of a sum of local energy potentials.8 V-JEPA 2 plans a real robot by minimizing an embedding-space distance — an energy — with cross-entropy method.9 In all three, energy is a scorer: what you minimize to act. None uses it as a Lyapunov certificate. (We did not originate "energy over diffusion," and we do not claim step-count wins are energy-specific — one-step flow-matching policies achieve comparable inference cost without energy.10)
The certificate as a separate object. The certificate community has the other half. Certified World Models place a Lyapunov-spectrum condition on the world model itself; differentiable reachability certifies to tens of state dimensions with hardware validation.11,12 But in every case the certificate and the action-objective are two separate scalars, trained by two separate mechanisms — deliberately, because an energy shaped for action selection and a valid Lyapunov function are, in general, different objects.
The unclaimed slot is their union: one scalar energy that is simultaneously (1) the action-objective, (2) a formal worst-case certificate checked before commit, (3) physics-structured, (4) priced in joules per task, and (5) continuously learned. Each face is occupied by strong work; the five-way intersection is empty. Our claimed edge is the unification, in the contact-rich regime — where equivariance-based certifiers are weakest — not raw dimensionality, where the adjacent work leads and that lead is not contested here.
3 · The mechanism, at nano scale
We test the load-bearing question directly. Take a 1-DOF hybrid contact system — a mass in free flight until a spring-damper wall switches on at $x=1$, under a constant inward bias — a nano stand-in for touching a surface against a preload. A single quadratic energy $E(s)=\lVert s-s^\star\rVert^2_P$ does double duty. The controller acts by one-step descent of $E$. The certificate coasts the committed action and checks that $E$ stays within a basin margin — a sampled contraction condition
The result, seed-deterministic and re-run independently: the certificate is real and binding — only 12.2% of controllers in the shared family pass it. And it discriminates. An outcome scorer — the realistic model of a vision-judge or sample-and-score world-model policy — crowns a rollout whose final frame looks like a near-perfect hit ($x=1.001$); coasting its committed action drives the state to leave the safe region at step 196 and keep growing. The certificate rejects exactly those plans.
Then we made it a proof. The greedy descent of a quadratic energy is a linear control law, so the closed loop is piecewise-linear across the contact switch. For that system we exhibit a common quadratic Lyapunov function $V(e)=e^{\top}Pe$, $P\succ 0$, and verify — exactly, by the eigenvalues of $A_i^{\top}PA_i-P$ in both the free and contact modes — that $V$ strictly decreases everywhere in a certified region of attraction:
with proven per-step contraction $V_{\text{next}}\le 0.989\,V$. This is linear algebra over the entire continuum of the sublevel set — not a sampled check — and the same $P$ is the energy the controller descends to act and the certificate that proves it cannot diverge. A sample can report "100% sound" and be wrong at the point it did not test; the eigenvalue condition cannot.
The same energy extends to a genuinely nonlinear system. For a damped pendulum ($\sin\theta$) under the same kind of controller, a quadratic energy certifies a region of attraction analytically — exact linear decrease $-\lVert s\rVert^2$ plus the bounded nonlinearity $\lvert\sin\theta-\theta\rvert\le\lvert\theta\rvert^3/6$ — proven for $\lVert s\rVert < 1.35$ rad over the whole continuum. A quadratic on a nonlinear plant certifies cleanly; where a quadratic cannot win is a non-convex region of attraction — and that is where a learned energy earns its keep.
We demonstrated exactly that, with a solver that cannot be argued with. On the reversed Van der Pol oscillator — whose region of attraction is non-convex, bounded by an unstable limit cycle — the δ-complete SMT solver dReal certifies the best quadratic energy to $R=1.1$ and refutes it at $R=1.2$ with a concrete counterexample. A learned energy — the certified quadratic plus a tanh correction, trained counterexample-guided against the solver in the Neural-Lyapunov-Control lineage14 — is certified to $R=1.3$: +18% radius, ~40% more certified area than any quadratic can prove. And the ternary version of that network ($W_1=s\,T$, $T\in\{-1,0,+1\}$, half its weights exactly zero) certifies the same $R=1.3$ — the 1.58-bit structure cost nothing. Three design choices made the synthesis converge where naive attempts stall: initialize the network at the certified quadratic so it learns only the shell beyond it; train to a margin several times stricter than the verifier checks, so the proof sits far from the δ-boundary; and isolate each solver query so a hard instance cannot stall the loop. $R=1.4$ did not certify — that is the boundary, stated plainly.
| policy (1-DOF hybrid contact toy, N-trial) | settled / held | drifted off | abstained + replan |
|---|---|---|---|
| sample-and-score (predict → act) | ~56% | ~44% | — |
| certificate-gated (predict → verify → act) | 100% | 0% on certified commits | ~50% |
Two qualifications we keep on the record. First, the cost of unification is not a fixed price: across three independent implementations it was moderate in one toy, vanished in a second (a selection artifact), and was protective in a third where the unconstrained controller diverged 20% of the time. We report the mechanism, not a tax. Second, both an outcome judge and a path-integral reward are fooled at nearly the same rate, because neither certifies what happens when the imagined window ends — the certificate does. That the two scorers fail alike is the sharpest form of the claim: a score over a finite window is not a certificate of the commitment.
4 · The certificate is cheap on ternary — the same structure twice
A certificate is only useful at the edge if it is cheap to run there, and here the Institute's two research lines meet. Bound-propagation — the certificate's core primitive — pushes an input interval $[\,c-r,\ c+r\,]$ through a linear layer as
For full-precision $W$, the radius update $\lvert W\rvert r$ is a dense matrix multiply — the same multiply that dominates neural energy.13 Write a ternary weight as $W = s\,T$ with $T\in\{-1,0,+1\}$ (BitNet absmean). Then $\lvert W\rvert r = s\,(\lvert T\rvert\, r)$, and because $\lvert T\rvert\in\{0,1\}$ the radius update is pure add / subtract / skip plus one scale — multiply-free. The 1.58-bit structure that deletes the multiply in the forward pass deletes it again in the certificate.
We verified this on a small network (seed-deterministic). The radius update that costs 512 multiplies in full precision costs 0 multiplies in ternary (355 adds + 3 scales; the zero weights are skipped outright). A quantified bonus, flagged as an absmean side-effect rather than a guarantee: because absmean quantization shrinks the row-$\ell_1$ norm that drives interval blow-up, the certified radius grew about 3× more slowly through the net than in full precision. Cheaper, and here tighter.
| certificate radius-update, one small net | multiplies | radius growth (4 layers) |
|---|---|---|
| full precision | 512 | 0.10 → 27.7 |
| ternary (1.58-bit, absmean) | 0 | 0.10 → 8.9 |
This is the Energy First Architecture's wager in one line: the same scalar energy is what the agent minimizes to act, what certifies its plan before it commits, what physics computes for it structurally, and what it is priced in watts to spend — and the ternary substrate makes the certifying as cheap as the acting.
5 · What certifies — and when
Carried across systems with the same score-first energy, one δ-complete SMT solver (dReal) and — where dReal saturates — a sound second-order Taylor model with adaptive refinement, the picture is a ladder, each rung a proof over the continuous state space, not a sample:
Show the computation
reversed Van der Pol: ẋ = −y, ẏ = x + µ(x² − 1)y (µ = 1)
certified ROA = the sublevel set {V ≤ c} that fits inside the true basin
quadratic V = xᵀPx → best inscribed ellipse, R ≈ 1.1
learned V (ternary net) → bends to the basin, R ≈ 1.3 (+18% radius)
both verified by δ-complete SMT (dReal) over boxes — proof, not sampling| system | what is proven | learned vs quadratic |
|---|---|---|
| 1-DOF contact (piecewise-linear) | common quadratic Lyapunov fn, exact by eigenvalues | quadratic suffices |
| damped pendulum (nonlinear) | analytic ROA ‖s‖<1.35 rad; dReal-certified region | quadratic suffices |
| reversed Van der Pol (non-convex ROA) | dReal certificate over the annulus | learned ternary R=1.3 vs quadratic 1.1 (+18%) |
| wall contact, mode switch | certified across the free/contact discontinuity | quadratic suffices in the unclamped strip |
| contact + actuator saturation (6-case) | learned ternary certified through saturation, R=1.2 | learned certifies where quadratic is refuted (R=1.0) |
| cart-pole (4 states, sin/cos — convex ROA) | quadratic certified over the 4D continuum to R=0.6 | quadratic suffices (Riccati anchor near-optimal) |
| coupled Van der Pol (4 states — non-convex ROA) | learned ternary certified over the 4D continuum, R=1.0 | learned R=1.0 vs quadratic R=0.8 (quadratic invalid past 0.9) |
Two results deserve to be named. First, 4D is reachable: naive interval bounds and dReal both choke on the 4-state quartic-plus-trig system, because the interval gradient of $\Delta V$ never lets $J_f^{\top}\nabla V(f)$ cancel $\nabla V(s)$. A second-order Taylor model fixes it — bound $\Delta V(s)\le \Delta V(c)+|\nabla\Delta V(c)|\,r+\tfrac12|H|\,r^2$ using the exact center gradient (which cancels to $\approx-2Qc$) and a Hessian that itself cancels to $\approx-2Q$ — so the bound converges as $O(h^2)$ and adaptive refinement certifies the whole continuum in seconds.
Second, the law, and it holds in both dimensions we tested. A learned energy certified strictly more than a quadratic in exactly the systems whose region of attraction is non-convex — and so cannot be captured by any ellipsoidal sublevel set: the 2-state Van der Pol (learned $R=1.3$ vs quadratic $1.1$) and, decisively, a 4-state pair of coupled Van der Pol oscillators, where the learned ternary energy is certified to $R=1.0$ over the full 4D continuum while the quadratic is not merely weaker but invalid past $R\approx0.9$ (19,149 decrease violations in six million samples of the $R=1.0$ region). On the smooth systems — pendulum, cart-pole — a quadratic built from the Riccati value function is already near-optimal (worst-case decrease ratio $+1.02$), and the learned correction, trained and quantized to ternary, collapses toward zero because there is no gap to fill; a tighter verifier changes nothing. The statement is therefore precise and now checked in 2D and 4D: the learned certificate earns its keep where, and only where, the safe set is non-convex. That is not a limitation of the method — it is a map of when to reach for it.
And the reach extends further than box-by-box refinement can. For polynomial systems, a Sum-of-Squares certificate verifies the whole region in a single semidefinite program rather than by enumeration — on chains of coupled Van der Pol oscillators we certified the region of attraction at 4, 6, and 8 states (2 s, 18 s, 198 s), where dReal already times out at 4 and interval refinement needs $10^{6}$-plus boxes. The two verifiers are complementary: SOS for reach (higher dimension, polynomial dynamics), the tight Taylor-plus-CROWN model for the non-convex, learned, and hybrid certificates a global SOS relaxation blurs.
And it is cheap. Measured on real silicon with a multi-domain, idle-subtracted, noise-floor-aware energy harness, running the certified ternary energy inside the control loop costs on the order of a microjoule per certified step — 0.0004–0.003% of a one-watt-per-joint actuation budget. Verifying every action before you commit to it is, in a robot's energy budget, free. (At this nano scale the per-step figure sits at the vendor counter's noise floor; the harness reports that, and ships an external-meter protocol for the precise number.)
6 · From proof to gate: verified correctness at deploy time
A proof that stays in a notebook changes nothing. The same score-first energy and the same dependency-free verifier are now a deployment gate in the Institute's open, pure-Rust edge-deploy stack (Ferralloy): a policy pack carries its Lyapunov certificate as a signed manifest facet, and before a device will trust the pack it re-proves the certificate on-device — the second-order Taylor + per-box CROWN pass, in pure f64 with nothing from the math library beyond tanh, no SMT or SDP solver present. The check is wired at every hop: at build (a bad certificate is rejected, naming the box where $\Delta V\ge 0$), at release, and — the one that matters — inside the device agent, which re-proves before a pushed pack goes live, exactly as it already byte-compares a signed behavior vector. Verified correctness alongside verified behavior.
Because the verifier is arithmetic and a box worklist, it runs where the robot runs. Compiled to WebAssembly it re-proves the non-convex Van der Pol certificate inside a browser/edge sandbox — the same result as native, in a 97 kB module — and the whole re-proof costs 0.08 ms (a smooth plant) to 1.5 ms (the nonlinear Van der Pol) measured in-process, paid once when a pack is accepted, not every control step (distinct from §5's per-step in-loop figure). A registry of certified systems sits behind one interface — a smooth double integrator (the quadratic suffices, empty head), a saturated one (a trained ternary head certifies where the quadratic is refuted at $R\approx0.8$), the hybrid wall-contact system, and the nonlinear Van der Pol — the §5 law made executable: the same gate accepts a bare quadratic exactly when the quadratic is enough, and demands the learned head exactly when it is not. Each certificate was soundness-checked against a Monte-Carlo ground-truth maximum before it was allowed to ship.
7 · One energy, both roles — and the tax is zero
Section 2's empty intersection turns on one claim above the rest: that a single scalar energy is at once the control objective and the stability certificate — and that forcing one energy to do both costs nothing. We measured it. On the saturated double integrator (where a plain quadratic certificate is refuted, §5) and a nonlinear torque-underactuated pendulum, one learned energy is a 100% controller and a soundly-proven, independently-audited Lyapunov certificate under its own greedy control, with a measured zero tax both ways — train an energy purely to certify and it still controls at 100%, because descending a control-Lyapunov function is a controller. And the certificate need not be proven box-by-box at all: structure the energy as a port-Hamiltonian and it holds by construction to a 24-dimensional state, where a box/SMT proof walls out at ~8D.
The full ladder — 2D→4D sound proofs, learned ≻ quadratic on a non-convex plant, the structural certificate off the toys, and a necessity gate that catches a real policy's out-of-distribution unsafe actions (envelope violations $2951 \to 0$, in microjoules, minimum-intervention) — is set out in the companion results paper: One Energy, Both Roles →.
The entity does not consult a model and then check a separate certificate. It descends one energy — and the same descent is the guarantee.
See it live: the saturated double integrator → · the nonlinear pendulum (the harder confirmation) →
the value-energy driving each plant to its goal by pure descent, with the proven Lyapunov basin drawn on the phase plane.
8 · Limits
The demonstrations here are nano and in simulation — 2 to 4 states, certified at solver precision $\delta$ around $10^{-3}$$–$$10^{-6}$ over annuli that exclude a small converged ball. The synthesis method is the Neural-Lyapunov-Control lineage (Chang & Gao); our contribution is the ternary leg, the quadratic-anchored initialization, the train-stricter-than-verify margin design, and the second-order-Taylor 4D verifier — not the CEGIS idea. Every "learned beats quadratic" claim is confined to the non-convex case (Van der Pol); on the smooth and hybrid systems a quadratic suffices and we say so rather than manufacture a use for the network — that restraint is the law of §5. One boundary named plainly: the learned net does not yet beat the quadratic in 4D — but that is the §5 law working, not a gap to close: the Riccati anchor is already near-optimal there, so no tighter verifier can manufacture an advantage. Where a real gap does exist — the saturated-contact regime, quadratic refuted at $R=1.0$ — a per-box CROWN relaxation of the tanh head certified the learned energy to $R=1.2$ where dReal went δ-hard, sound over $4\times10^{6}$ sampled checks; $R=1.3$ is the genuine refutation boundary. None of these energies has run on a real robot; the joules figures use a vendor RAPL counter at whose noise floor the per-step signal sits (hence the external-meter protocol we ship); and nothing here is independently replicated, the same caveat we apply to everyone. We price every limit, we do not claim to beat frontier systems at scale, and we do not claim drift is impossible — only that it is structurally bounded and, here, caught before commit, over the whole continuous state space, in seconds. The deploy gate of §6 is built, tested (unit, device-side accept path, and executing in a wasm sandbox), and its re-proof is measured — but it has not yet gated a pack on a physical robot, and its open-source release is in progress; the claim is that the on-device re-proof is sound and cheap, not that it has been field-hardened. The §7 zero-tax result is likewise nano and single-seed: the double integrator is saturated-but-otherwise-linear, where the value-function/Lyapunov coupling is expected (LQR) — the contribution is that it survives saturation with a learned energy, a sound proof from both training directions, and a measured zero tax, with the nonlinear pendulum as the harder confirmation; whether the tax stays zero on a contact-rich, higher-DOF plant is open.
References
- NVIDIA, Cosmos 3: Omnimodal World Models for Physical AI, arXiv:2606.02800, 2026.
- Yang et al., WorldGym / World-Gymnast, arXiv:2506.00613, 2602.02454.
- WorldVLA, arXiv:2506.21539, 2025.
- Physical Intelligence, π\*0.6 / RECAP, arXiv:2511.14759, 2025.
- SafeDreamer (PKU); Cosmos Policy (NVIDIA), 2026.
- Google DeepMind, Genie 3, 2025–26.
- Davies, Huang, Gladstone et al., EBT-Policy: Energy Unlocks Emergent Physical Reasoning, arXiv:2510.27545, 2025.
- Sun, Mishra, Lu, Xu, Armeni, Energy-based Compositional Diffusion Planning, arXiv:2606.21646, 2026.
- Meta FAIR, V-JEPA 2, 2025.
- FlowPolicy (AAAI 2025), arXiv:2412.04987; MeanFlow/MP1, arXiv:2507.10543.
- Wang, Certified Predictability for Equivariant World Models, arXiv:2606.13092, 2026.
- Chou et al., Pixels-to-Proofs / differentiable reachability, RSS 2026.
- Horowitz, Computing's Energy Problem, ISSCC 2014 (op-energy constants); BitNet b1.58 (absmean ternary), 2024.
- Chang, Roohi & Gao, Neural Lyapunov Control, NeurIPS 2019; Gao, Kong & Clarke, dReal: An SMT Solver for Nonlinear Theories over the Reals, CADE 2013 — the counterexample-guided synthesis method and δ-complete verifier our learned-ternary certificate builds on.