drorb · a formally verified network engine, in Lean 4

The fix is
a theorem.

Most fast network stacks ask for your trust: they parse your traffic, terminate your TLS, route your requests, and you take their word that they did what they said. drorb hands you a proof instead · a reverse-proxy whose behaviour is stated and proved as theorems, machine-checked by the Lean kernel, and driven over real sockets by an untrusted IO shell that never touches the proven core.

The wire, as theorems.

HTTP/1.1. HTTP/2 · framing, HPACK, streams. HTTP/3 and QPACK. QUIC. TLS 1.3. WebSocket. DNS parsing, SSE, 103 Early Hints. Each one lives in the engine as a total transition system with safety theorems · well-formedness, framing, in-bounds, termination.

For the HTTP/1.1 parser the claim is upgraded from safety to correctness: the request-line and header fields resolve to exactly their input bytes · not just in-bounds, but right. The same soundness is proved for the HPACK and QPACK literal field case. And the honest boundary, said plainly: most lanes are safety-only so far. The safety-to-correctness upgrade is ongoing, not finished.

Routing has a stronger property than a filter: a literal ../ escaping the root is impossible, not caught. The JWT algorithm-confusion vulnerability is proven absent. The kernel-lending ring at the bottom recycles every buffer exactly once, under every adversarial interleaving · including ones no test would reach.

GET /health          → 200, with HSTS + security headers (proven stages)
GET /admin           → 401 (the real JWT gate short-circuits)
GET /..%2fetc/passwd → 404 (a literal ../ escaping the root is blocked, not filtered)

We attacked our own server.

HTTP response splitting is an old class of bug: if a server will echo a carriage return where one doesn't belong, an attacker can end your response early and write their own. We went looking for it in drorb · and found it, real and demonstrated, on our own shipped reactor.

A hostile upstream got a stock curl to read an injected Set-Cookie · and then a whole second response · out of a response head drorb never saw those fields in. Session fixation, on a reachable configuration. No advisory, no CVE, no one else's report: our own red team, against our own engine.

The fix did not go in as a patch. The default forwarding path gained a gate, and the guarantee about every emitted head · that the client parses exactly what the proof says it parses · was re-proved through the gate. When the same shape turned up on an opt-in seam path, that was closed too, and the stream-faithfulness theorems were restated under the gate rather than loosened around it.

Finding it ourselves, first, is the whole game.
The fix is a theorem, not a patch note.

A tailnet with a proven coordinator.

drorb also speaks the Tailscale coordination protocol · as the control plane, not a client. A stock tailscale client, unmodified, enrolls against it:

tailscale up --login-server=https://drorb/     (keyless)
  → AuthURL issued
  → drorb-ctl approve
  → node authorized · Running · 100.64.0.4 allocated
  → key self-expiry → live re-auth

The netmap the client receives carries its peers, a DERP map naming drorb's own relay, and a packet filter that is not derived from the ACL policy but proven equal to the ACL compiler's output · the served filter is a theorem about the policy file. Key expiry is enforced; pushes are targeted. What stands demonstrated here is control-plane truth: enrolment, policy, the map.

The floor under the crypto.

House rule, standing: verified-Lean or audited primitives only. Nothing else ships. TLS 1.3 and QUIC key schedules run over verified EverCrypt/HACL* · the assumed properties are theorems proved upstream, not hand-waved.

And the post-quantum surface went further: every PQ operation in the stack · verify, sign, encapsulate, decapsulate, and both keygens · dispatches a verified core. No crate-authoritative PQ path is left. The claim is checked against the artifact, not the source tree: the shipped release binary confirms all six verified cores by symbol inspection, openssl-free. The Keccak permutation underneath refines FIPS 202. An audited dependency was the floor; this is the ceiling.

What is trusted, named.

The theorems are about the models, and two things are trusted out loud: the Lean kernel · small, audited, published · and the IO shell: the socket, accept loop, and connection lifecycle. The shell is validated by testing; everything above it is proved. That boundary is stated in the README rather than discovered in an incident report, which is the difference this project exists to demonstrate.