The questions that should be asked first

Why not seL4? It's already verified.

It is, and indeed more thoroughly than we will be for a long time: functional correctness, integrity and noninterference, carried down to the binary, with the assumptions written down. If what you need is a verified kernel, use seL4.

It answers a different question, though. seL4 proves that a kernel correctly enforces the capability distribution you configured, but it has nothing to say about whether that distribution is the right one, and nothing at all about velocity ceilings, stopping distances or Cartesian keep-out regions, none of which are operating-system concepts.

The deeper mismatch is placement: a verified kernel runs on the same machine that is planning the motion, whereas our claim rests on the actuator lines terminating somewhere that machine cannot reach at all. No kernel can give you that property, because it is a property of the wiring.

Why not WebAssembly and a capability-based host?

It is a genuinely good answer to a neighbouring problem, and we would be foolish to pretend otherwise. WebAssembly has a mechanized specification with soundness proofs, deterministic fuel metering in production, and an interface model where a component's entire authority surface is declared statically.

What it does not have is any constraint between the capabilities it grants. Nothing in the component model prevents data read through one import from leaving through another; there is no policy logic for temporal, conditional or quantitative limits; and admission is type-checking, not proof. Academic work has shown information-flow control over WebAssembly is buildable, and equally that nobody has shipped it in an engine.

It also runs on the agent's computer, which is the recurring answer to most of these questions: a software boundary inside a compromised machine is a boundary the attacker is already standing behind.

Why not a safety PLC, or the safe-motion functions in my drive?

Of course, if you have them, use them. We say this on the front page and we mean it commercially: a cell running certified dual-check safety or safe-motion supervision already has a validated envelope, and it already lets the motion program change without revalidating the safety configuration. An agent writing programs into that cell is already bounded.

Two things remain. Those systems were designed against programmer error, not against a program source under adversarial control, so the integrity of the command channel is assumed rather than enforced, and none of them produce a signed record attributable to the entity that issued each command. And they do not exist on the platforms where language models are being deployed: quadrupeds, humanoids, research rigs, mobile robots and custom actuator setups ship with no safety-rated envelope at all.

Why not a software guardrail on the agent host?

Largely because it shares fate with the thing it is guarding. A policy engine, a plan validator or a temporal-logic monitor running in the same process tree as the agent is subject to every compromise the agent is. Several published systems in this class also place a language model inside their own trust boundary, which means the guardrail can be argued with.

They are useful, and they generally lower the rate of bad plans; a good deployment typically runs both. They are not a bound, because a bound has to be something the bounded thing cannot modify.

What if the gate itself has a bug?

Assume it does. The design assumes it too.

• The emergency-stop chain is wired physically around the gate, in series with the contactor coils. No firmware state can command motion.
• The envelope monitors are native code outside the interpreter, so a fault in program execution does not reach the limits.
• Every failure path denies rather than permits. A malformed program, an exhausted fuel budget, a checksum mismatch and a watchdog timeout all produce the same outcome: a safe stop.
• The trusted base is roughly 550 lines, published, and small enough that a third party can actually read it. That is generally the point of keeping it small: auditability rather than elegance.

What we do not offer is the claim that it is bug-free. Verification covers memory isolation and absence of undefined behaviour in the interpreter core. The monitors are engineered and model-checked, not proven, and we label them that way in the architecture.

Doesn't proof-carrying code solve this properly?

We designed the product around it, then removed it. The short version: for a per-program certificate to mean anything you must formalise the interpreter's semantics and prove the interpreter implements them, which is the whole proof obligation of verifying the interpreter on its own. The certificate design is therefore the simpler design plus a checker, a proof format, and an encoding-soundness argument.

Proof-carrying code exists so untrusted code can run at native speed without runtime checks. We interpret and clamp anyway, so it buys nothing here. The full reasoning and the empirical confirmation are in the research record.

Why talk to a company with no product?

Largely because the design decisions that matter are being made now, and a design partner with real hardware tends to change them. Two of the six reversals in our research record came from exactly this kind of contact with reality.

What we can offer today is the analysis rather than the device: threat modelling for a specific deployment, safety-case structure for a model in a control loop, and architecture review. That work stands on its own and is how most engagements start.

Why not just send parameters to a fixed program?

Our working hypothesis is that the interpreter earns its place through conditional reaction that cannot survive a round trip: deciding locally that a force threshold has been exceeded and retrying from a different approach, rather than asking a machine that may be compromised, or merely late. As parameters, that requires enumerating every branch in advance.

It is a hypothesis. It needs one customer with a real application to confirm or kill it, and if it is killed we will cut the interpreter exactly as we cut the proof checker. That is stated as an open problem rather than resolved in our own favour.