Your AI agent doesn't have to escape the sandbox to hurt someone.
It only has to be tricked while holding permissions you correctly gave it. Endstop is the hardware that bounds what it can actually do.
Containment is not safety
Agents now act — running code, moving money, driving actuators — faster than anyone reviews what they do. The exposure isn't who wrote the code. It's that nobody approved the effect.
Sandboxes are good at what they do. seL4 is machine-checked down to the binary.1 WebAssembly has a mechanized specification. gVisor and Firecracker are what the frontier labs actually run. None of that is the problem.
The problem is that a sandbox bounds where computation can reach — not what legitimately granted authority can do. An agent holding a database read and an API call can exfiltrate without escaping anything. An agent holding an actuator can wreck a gearbox while every speed limit is satisfied, or sweep a tool through the space a person is standing in while every joint sits inside its own envelope.
This is not a new class of defect. It is the confused deputy problem, described in 1988.2 What is new is that the deputy now takes instructions from whatever text it happens to read — and that researchers have demonstrated a 100% jailbreak rate against commercial robots shipping today.3
Untrusted planner. Verified supervisor.
This architecture is not our invention, and that is precisely the point.
Industrial robotics has shipped it for years and had it type-certified. On an ABB system, one component plans the motion — and the manual states plainly that it is not a safety function. A second, safety-rated component supervises every command and stops the machine when the first one is wrong. During validation the planner is switched off entirely, because what you validate is the supervisor.4
Our change is a single substitution: the planner is now a language model.
Everything else follows
You do not have to trust the model. You do not have to review its output. You do not have to believe anything about how it was trained. You have to bound what it can cause — and that bound has to live somewhere the model cannot reach.
A gate that holds the authority
A small module between the agent's computer and the things that matter. The actuator lines — or the signing key — are wired to it, not to the machine running the model. The agent proposes. Only the gate acts.
It runs a formally verified core on a soft processor with no operating system, no DMA and no network stack. Programs execute under a fuel bound, so they terminate by construction. Effects exist only as entries in a fixed capability table — anything outside it is not refused, it is unrepresentable. Every proposed command is checked against an envelope validated offline, and anything outside it degrades to a safe stop rather than being held.
| Parameter | Design target |
|---|---|
| Trusted computing base | ~550 lines |
| Interpreter core | machine-checked, published5 |
| Effect vocabulary | 3 capabilities |
| Enforcement | every control cycle |
| Added latency | < 100 µs |
| Guard-distance cost | ≈ 0.16 mm6 |
| Termination | fuel-bounded, by construction |
| Audit record | Ed25519-signed, replayable |
| Emergency stop | wired around the gate |
That last line matters more than the rest. The gate can only ever permit motion. It can never force it. How it works →
Signed evidence of what the model actually did
Every command the agent issued, and every limit that refused it, written to a tamper-evident, replayable record — produced by hardware the agent cannot reach or alter.
This is what you need the day after an incident, when every other log lives on the machine that failed. Aviation has flight recorders. Trucking has tachographs. Payments have hardware audit logs. Autonomous machines driven by language models have nothing.
Where it applies
Built for
Humanoids, quadrupeds, research VLA rigs, mobile robots, drones and custom actuator setups — the platforms where language models are actually being put in the loop, and where the only measures available today are a person on the e-stop, staying in simulation, or hoping.
Not for
Certified industrial cells. If you run FANUC with DCS or ABB with SafeMove you already have a validated envelope, and you should use it. Those systems already let the motion program change without revalidating the safety configuration.
We will tell you that rather than sell around it.
Status, stated plainly
In this field the distinction between what is proven, what is engineered and what is assumed is not a footnote. It is the entire product.
- Proven
Memory isolation and absence of undefined behaviour in the interpreter core — machine-checked, published, independently reviewable.
- Engineered
Envelope monitors, capability mediation and the signed audit chain. Verified by testing and model checking, not by proof.
- Assumed
The hardware model, the synthesis toolchain, and the absence of a physical attacker. Each is stated, not buried.
- Not claimed
No safety certification. No proof-carrying admission. No guarantee that a correctly-configured envelope is the right envelope — that remains a risk assessment, and it remains yours.
We also publish the questions we have not answered. Our open problems →
References
- Klein et al., seL4: Formal Verification of an OS Kernel, SOSP 2009; proof inventory and stated assumptions at sel4.systems/Verification/proofs.html.
- Hardy, The Confused Deputy, ACM SIGOPS Operating Systems Review 22(4), 1988. doi:10.1145/54289.871709
- Robey et al., Jailbreaking LLM-Controlled Robots (RoboPAIR), 2024. 100% attack success against NVIDIA Dolphins, Clearpath Jackal + GPT-4o, and Unitree Go2. arXiv:2410.13691
- ABB, Application manual — Functional safety and SafeMove2, 3HAC052610-001; and Functional safety and SafeMove (OmniCore), 3HAC066559-001. The planning component is documented as not being a safety function; the safety-rated supervisor is the backstop.
- Yuan et al., End-to-end mechanized proof of an eBPF virtual machine for microcontrollers (CertrBPF), CAV 2022. Coq-verified VM deployed in RIOT OS on RISC-V targets.
- ISO 13855 prices reaction time at an approach speed of 1600 mm/s, giving 1.6 mm of required separation distance per millisecond of latency.