Including the parts where we were wrong

What this is built on

Almost nothing here is new in isolation. The contribution is the combination and the artifact, and it is worth being specific about whose work it rests on.

Where we differ from the industrial precedent is narrow and specific: their planner is a deterministic motion program written by an engineer, and ours is a language model driven by text an attacker may control.

Corrections

Six positions we held, published internally, and then reversed on evidence. Each is dated to the review that overturned it.

We cut the proof checker we designed the product around

The original architecture had every agent program arrive with a machine-checkable certificate, validated on-device. Adversarial review killed it. For a certificate to mean anything you must formalise the interpreter's semantics and prove the interpreter implements them — which is the entire proof obligation of simply verifying the interpreter. The certificate architecture is therefore the verified-interpreter architecture plus a checker, a proof format, and an encoding-soundness argument. Its trusted base strictly contains the alternative's.

Proof-carrying code was invented so untrusted code could run at native speed without runtime checks.¹ We interpret with fuel and clamp every effect, so we would have paid its whole cost for none of its benefit. The empirical confirmation is recent: Cranelift's proof-carrying-code implementation was removed from Wasmtime in 2026 by its own author after it bit-rotted, never having been enabled by default.

We said information flow was impossible, and that was wrong

An adversarial review established that noninterference is a hyperproperty and therefore not enforceable by monitoring a single execution — correct as stated, and we published it. Subsequent work showed the conclusion does not transfer to our setting: those separation results rest on undecidable halting, and under a fuel bound every execution is finite. Termination-insensitive noninterference is 2-safety and reduces to a safety property of the self-composition.²

We record both the claim and its reversal, because the intermediate position was stated with more confidence than it deserved.

Our chosen robotics integration point was physically impossible

We selected 500 Hz setpoint gating on industrial and quadruped platforms on control-theory grounds — correct reasoning about where a gate can sit without destabilising a loop. Feasibility review then established that the target board has no Ethernet interface, while those platforms speak DDS or TCP protocols requiring a full network stack. Putting a general-purpose computer in the path would place the gate behind the untrusted machine, defeating the entire architecture. The pilot moved to PWM passthrough.

A performance figure was wrong by roughly fifty times

We recorded signature generation at one to two seconds, and designed around it. Benchmarking established that the figure belonged to a different, much slower library; well-configured portable code on the same class of processor is roughly twenty-five milliseconds. The error had a real consequence — it would have driven an unnecessary hardware decision.

Our envelope design was non-conformant

The initial monitor used per-axis position and rate clamps. Reading the collaborative-robot technical specification showed that a scalar limit on a single point is explicitly insufficient, in the standard's own normative note. The monitors became multi-point, with predicted stopping position rather than instantaneous clamping.

We ranked our markets by the wrong criterion

Financial signing ranked first on speed-to-pilot, because it needs no certification. Security review showed the pilot's threat model — which excludes physical attackers and side channels — is not merely weaker there but disqualifying, since tamper response is a baseline requirement for payment hardware. The fenced robot cell became the first market because it is the one where our exclusions are defensible.

Open problems

These are unresolved. Publishing them is not modesty; it is the only way the rest of this site can be read as calibrated.

Does the interpreter earn its place?

This one governs the product. Our own adversarial review posed it and we cannot yet answer it: name one policy a customer will pay for that is enforceable on a single execution and is not enforceable more cheaply by a fixed set of parameters passed to a fixed on-board program.

If no such policy exists, the interpreter should be cut exactly as the proof checker was, and the product is the supervisor alone — smaller, cheaper, and far easier to certify. Our working hypothesis is that conditional reaction without a round trip is the answer — "if contact force exceeds a threshold, retreat and retry from another angle" decided locally rather than after a round trip to a machine that may be compromised or merely slow. That is a hypothesis awaiting a design partner, not a finding.

Unmeasured and unclosed

• Timing closure on the target device is projected, not measured. The published latency budget is a design target.
• The verified interpreter is published under a copyleft licence, which has to be reconciled with product licensing before it can ship.
• No trademark clearance search has been completed for the product name.
• Certification cost and duration are unquoted, and we decline to repeat industry folklore about them.

Why we publish this

Every vendor in this space asks to be trusted. Very few show their working, and almost none show the parts that did not survive contact with evidence.

The audience for a device like this is people who read datasheets adversarially and who have been burned by confident claims. For them, a visible reversal is stronger evidence of method than any unfalsifiable assurance — and if we are wrong again, this is the page that will say so.