III / the orb · drorb
the wire
shook back.
Every fast network stack on earth asks for the same thing: your trust. It parses your traffic, terminates your TLS, routes your requests — inside a black box running millions of lines nobody has read. Dragon's Orb is the edge engine that hands you a proof instead: stated and machine-checked in Lean 4, driven over real sockets by an untrusted IO shell that never touches the proven core.
another program's verdict
Every green below is a reference implementation's judgment on drorb — not our own test suite grading our own homework.
- h2spec — 145/146 HTTP/2 conformance
- aioquic — completes a 1-RTT QUIC handshake, receives an HTTP/3 body
- testssl — grades the TLS 1.3 surface A+
- dig — 56/56 DNS on the wire
- nginx — load-balancer output byte-identical
- kernel WireGuard · aiortc · derper — Noise IK both ways · a real DataChannel message · DERP relayed
- 45/46 conformance scenarios pass against the real binaries — 0 unwired, 1 skip, named
- an mTLS auth-bypass — accepted without CertificateVerify
- OCSP revoked-staple acceptance — freshness checked, revocation not
- a hop-by-hop header leak — Connection not honored
- each found by a correctness lane, closed in the deployed engine, re-audited closed
- twelve deployed defects total — surfaced by rebinding proofs to the shipped gates, not by tests
That second panel is the whole argument for verification-over-testing — and the machine produced it empirically.
one orb, the whole surface
the wire
HTTP/1.1 · H2 · H3/QUIC · WebSocket served concurrently through one proven 13-stage pipeline; TLS 1.3, DNS, SSE, early hints — each a total transition system with safety theorems. The HTTP/1.1 parser is upgraded to correctness: it provably resolves exactly its input bytes.
the fabric
Routing where path traversal is impossible, not filtered · load balancing · health checks · circuit breakers · rate limits · sticky sessions · graceful drain · a chunk-boundary-safe streaming HTML rewriter · a response cache with request coalescing.
the vault
mTLS · ACME · Certificate Transparency · per-tenant isolation · the JWT algorithm-confusion vulnerability proven absent · TLS/QUIC key schedules on verified crypto (HACL*/EverCrypt) — the assumed properties are theorems proved upstream.
the floor
An io_uring-style ring modelled as a two-player game: every buffer the kernel lends is recycled exactly once, under every demonic interleaving — including ones no test would reach. A real io_uring dataplane drives the proven serve on Linux.
By the numbers, in the cut: 402 Lean files · ~4,500 theorems · 53 dedicated correctness lanes · #print axioms clean — zero sorry, only core axioms plus the named crypto carriers. Build it yourself: orb/build.sh, operator guide and systemd unit in orb/deploy/.
taking the compiler out of the trusted base
The deepest frontier, public as orb-compiler/ — heavily work-in-progress, and worth watching.
Today the proofs stop at the Lean source: you still trust the Lean compiler to translate it faithfully. orb-compiler is the descent past that — serve fragments emitted to a first-order systems language and proven, in an independent prover against the real backend-correctness theorem, that the machine code refines the spec. The technique already reaches real deployed code: a redirect decision, four serve-stage guards, and the cache-key hash fold that runs on every request — each closed end-to-end with zero axioms.
- the first full spec→machine-code theorem — a complete descent, 0 axioms
- the loop-free class, automated — what took a 629-line bespoke proof now closes in ~2 tactic lines
- real serve fragments — deployed decisions and the per-request hash fold, proven at the machine-code level
- the whole serve — composing the full stage pipeline is not done
- general loops — DEFLATE, the JWT state machine, CIDR matching
- the deep one — a verified data-layout and heap story for algebraic datatypes