Architecture

The authority lives on the other side of the wire

The agent computes wherever it likes, at whatever speed it likes, on hardware we assume is compromised. What it cannot do is reach the actuator lines, because they terminate at a different device.

§0

System definition

Endstop is a specified system with a proven core, not a concept awaiting design. What follows is its configuration, subsystem by subsystem, with the maturity of each stated rather than blurred.

Subsystem	Specification	State
Host processor	in-order RV32 soft core; no OS, no DMA, no network stack, no cache by default	selected · available
Interpreter core	fuel-bounded bytecode VM with memory-region isolation¹	proven · runs today
Capability table	three typed effects: read state, propose setpoint, request signature	specified
Envelope monitor	multi-point limits, predicted stopping position, rate ceilings, deadman	specified
Effect construction	trusted-side serialisation from an enumerated intent set with quantised parameters	specified
Audit chain	Ed25519 over program hash, monitor verdicts and a monotonic counter	specified
I/O surface	serial in; PWM or step/direction out; relay drive in series with the safety chain; SPI secure element	specified
Enforcement latency	< 100 µs per cycle at 500 Hz	projected · not yet measured
Board integration	bring-up, timing closure, end-to-end measurement	in build

The distinction that matters in that last column: the interpreter core is not something we intend to verify. It is demonstrably verified, published, and running on processors of this class today. The work in front of us is integration and measurement, not proof.

§1

The effect path

Every effect in the system follows one path, and there are no side doors — not because they are blocked, but because the instruction set does not contain them.

The agent (114), running off-board on untrusted host compute (110), sends a program over a unidirectional serial interface (120).
The program executes in the verified interpreter (134) under a fuel bound. It terminates by construction; there is no analysis to defeat, only a counter that reaches zero.
It may invoke exactly three capabilities through the capability table (136): read state, propose a setpoint, request a signature. There is no file, no socket, no allocator, no fourth verb.
Each proposed effect is checked by the envelope monitor (138) against limits validated offline, covering multi-point position, predicted stopping position, rate ceilings and a deadman.
Effects that pass are constructed by the trusted side and emitted (144) to the driver stage (152). Effects that fail degrade to a safe stop. Both outcomes are signed by the audit signer (142) under a key held in the secure element (140).

Figure 1. The effect path, with reference numerals. Authority terminates at the gate (130) rather than at the host (110); the host reaches the actuator plane (150) only through the gate; and the safety chain (160) bypasses the gate entirely, interrupting the servo drive (154) in series. A numeral key lists all twenty references.

The e-stop is not in this list

The emergency-stop chain (160) is wired physically around the gate, opening the contactor (164) in series with the servo drive. This is the one property we state without qualification. The gate can only ever permit motion. No firmware state, and no failure of ours, can command it.

§2

Two timescales, because the physics demands it

Fast control loops are certainly not ours to sit inside. Current loops typically run at 8–20 kHz and velocity loops at around 5 kHz, inside the servo drive where they belong. What crosses the network is setpoints, typically at 500 Hz or as PWM.

Figure 2. Where the gate inserts. The loops that stabilise the machine run at kilohertz rates inside the drive and never traverse the gate, so it cannot destabilise them. Only the setpoint stream crosses the boundary.

So enforcement splits. The slow path validates the envelope offline, once, the way every certified safety configuration in industry is validated. The fast path is a constant-time comparison against that envelope on every cycle, using table lookups with no allocation and no search.

Path	Rate	Work	Budget
Offline validation	per configuration	envelope derivation, risk assessment, signed acceptance	hours
Admission	per program	capability grant check, dry run under fuel	seconds
Enforcement	every cycle	multi-point limits, stop prediction, rate, deadman	< 100 µs

The latency figure is not chosen for marketing. ISO 13855 converts reaction time directly into required guard distance at 1600 mm/s of human approach, which works out at 1.6 mm per millisecond. A sub-100 µs budget costs about 0.16 mm of separation. The gate does not take workspace away from you.

§3

The trusted side constructs the effect

This is the design decision that came directly out of adversarial review, and it replaced an earlier design that inspected agent-supplied bytes.

A gate that validates a byte string is validating a field it believes is the amount, the joint index, the destination. Encodings tend to be adversarial: the same bytes often mean different things under different parsers, and the attacker chooses the encoding.

The agent supplies an index into a pre-approved intent set and quantised parameters. The gate serialises the transaction or the setpoint itself.
Effects are named, not described

Quantisation is probably as important. Snapping parameters to a coarse grid and emitting on a fixed schedule reduces the bandwidth of any channel an agent might modulate, from arbitrary to countable. We would rather publish a residual figure than imply zero.

§4

What is trusted, and what is merely present

A trusted computing base is only meaningful if you enumerate it. Ours is roughly 550 lines, and the parts outside it are listed with equal precision.

Component	Status	Basis
Interpreter core	machine-checked	published verified VM; UB-freedom and memory containment proven¹
Fuel accounting	machine-checked	part of the verified VM; a counter, not an analysis
Memory isolation	machine-checked	proven: all accesses land in designated regions
Capability table	engineered	static; callee behaviour not proven
Envelope monitors	engineered	native code outside the VM; model-checked arithmetic
Audit chain	engineered	Ed25519 over program hash, verdicts, monotonic counter
Boot & signature check	engineered	immutable first stage, anti-rollback counter
Soft processor	assumed	in-order RV32, no speculation, no cache by default
Synthesis toolchain	assumed	open toolchain, reproducible builds intended
Physical access	out of scope	no tamper response in the pilot

Figure 3. Scope of assurance. Only the innermost band is proven. Each band outward is a weaker claim, and the outermost is explicitly excluded. A trusted computing base is only meaningful if the exclusions are named.

Threat model exclusions

The pilot excludes physical attackers, power and electromagnetic side channels, and the gap between a formal hardware model and delivered silicon. Those exclusions are disqualifying for payment-HSM and cross-domain defence use, where tamper response is a baseline requirement — so we are not selling into those markets.

They should be defensible for a fenced robot cell, where physical access is already controlled, and that is the market we are addressing first.

§5

Deliberately small, deliberately dull hardware

An in-order RISC-V soft core on an FPGA, running from on-chip memory. No operating system. No DMA engine. No network stack. No cache by default, so timing is predictable and the speculative-execution attack classes do not exist to begin with.

The I/O surface should be the complete effect vocabulary: a serial link in, PWM or step/direction out, a relay drive that sits in series with the existing safety chain, and an SPI secure element holding keys. Everything the device can do is visible on the pin map, and that is what makes an independent audit tractable rather than aspirational.

Signing runs off the control path entirely. Verified portable code on this class of core generally signs in tens of milliseconds, and the control loop never waits on it.²

References

The interpreter core derives from a published, independently reviewable verified bytecode virtual machine whose machine-checked proofs cover absence of undefined behaviour and containment of memory accesses within designated regions. The specific artifact and its proof development are disclosed to design partners under evaluation agreement.
Measured figures for portable verified Ed25519 implementations on 32-bit RISC-V are approximately 1.2 million cycles per signature, placing signing in the tens of milliseconds at typical soft-core clocks. Implementation choice materially affects this; some widely used portable libraries are an order of magnitude slower on 32-bit targets.