Bugs? Rebuild it from a contract. Case study.
Much of security work on old software is a loop: someone finds a bug, someone writes a patch, and the patch is new code that can hold the next bug. The loop does not end, because nobody can say what the program does for every input. For C, the general question is undecidable.
Recently, it became much easier to find bugs, where the question is "find a single example of input where this software misbehaves", also known as FindInstance or exists quantifier.
But fixing these bugs became more expensive than ever; both due to volume and the depth of these overlooked issues.
This work attempts a different way: Do not ask a prover to understand the old program. Instead, write the program again, from a contract, and use only building blocks that a prover can check. I tried it on a real practical VPN app
The code and all reports are public: github: source code : zerotier-leaf-c. The full report has the method, the tables, the failures and the limits.
Writing software is cheap now. Leave the patch loop. Rebuild from a contract.
The idea
Machine learning did not win by training arbitrary programs. It won with a restricted set of functions over real numbers: the differentiable ones. Inside that set one tool, the gradient, works on everything.
The same move in two fields: restrict the functions, and one tool works on all of them.
Hence, the concept: Make a program out of a subset of primitives, that are easy to reason about; set of primitives over integers.
Some of the desirable properties of primitives in question include:
- its state has a fixed size: no heap;
- every loop has a bound that is written down;
- no primitive calls itself
- DAGs only, no recursion;
- Note that some recursion patterns can be converted to iteration or shortcut completely, but the general principle is that this should be done at implementation-writing time rather than at theorem-proving time
- no call goes through a pointer;
- no sum, product or conversion wraps around or loses bits;
- it has a contract: what it may read, what it may change, and what is true when it returns.
For such functions, today's automatic provers decide "the code meets its contract" for every input, not for the inputs of a test. This means, that there are by construction, no "special inputs" that would cause the program to misbehave.
The set does not hold every program.
The bet is, that it holds enough to build useful things.
It is expected that over time, these rules may be relaxed as the fundamentals of integer mathematics improve. For now, they are what they are.
The worked example
ZeroTier is an overlay network, aka a VPN with built-in NAT traversal. Nodes anywhere on the Internet behave as if they were on one, local Ethernet.
the IP packets of the internal network get packaged into UDP datagrams with an authentication code and an encrypted Ethernet frame inside. The official client/server implementations are a (relatively for microcontroller scale) large C++ programs.
Accommodating my private budget constraints, I decided to write a restricted version of the client, that is just enough for a small sensor node.
A sensor node does not need all functionality of a full client. It needs the leaf role: talk to a few known peers, relay for nobody.
Using LLM agents, I wrote that role again in plain C, from the wire format, for a microcontroller, with the following design limitations: * 7 pinned peers * one network * no heap
Result: about 2,500 lines in 9 files.
For comparison I also ported the core of the official client (ZeroTier One 1.16.2) to the same board, a Teensy 4.1 running Zephyr; an earlier post describes that port. The port and the rebuild together took about two weeks of work.
What "checked" means here
Every function comes with a contract. Three kinds of evidence stand behind it.
- Deductive proof (Frama-C WP with three automatic provers): 4,296 goals in a 64-bit model of C and 4,301 in a 32-bit model. All proved, at the full packet size of 2,048 bytes. Goals include no run-time error, no read or write outside the named memory, no arithmetic that wraps, every loop ends, etc.
- Proofs about the design, not only about safety. Goals include: no frame reaches the host, and no reply leaves, unless exactly one authentication call answered "yes" with the key of a pinned peer; Every packet takes exactly one packet number (it is the nonce of the encryption); What the client sends, its own receive path reads back unchanged; and more.
- Deliberate errors. A contract can say too little, and then the proof is worth little. To test the contracts (test the tests!) I put 104 wrong versions of the code into the sources, one at a time; injected bugs include: a compare that ignores the last byte; a nonce that does not advance; a missing bounds check. The tool that should see each bug, successfully rejected them in 118 of 118 runs.
One full proof set run takes about 32 minutes on a 32-core machine. The deliberate errors take about 2 hours more.
What the proofs found
Compared to the reference solution, and 'first try, source inspired' rewrite, I have kept a list of every place where a contract became stronger, with the wrong program that it accepted before: 30 entries so far. These include:
- A proof that compares the sender with the receiver did not go through. The reason: a node whose own address starts with the byte
0xffwould send packets that every receiver takes for fragments. Real addresses never start that way, but nothing in the code said so. No test had found it, because tests use valid identities. - Three functions that build answers said nothing about the packet number. Function by function, a version that used two numbers for one answer would have passed. The caller's proof failed until each contract said it.
- The compiler replaced the loop that wipes key material with a library call, and may delete such writes. No prover sees that: provers read C, not machine code. The build now fails if a wipe does not survive.
Note that none of these change the protocol; the implementation merely became much more strict.
As of 2026-11-14, it is unclear if any of these could be used to exploit the original client; more research pending. Exciting!
The price, measured
I expected the new, proved code to be slower. After all, this new code is written for the provers, not for speed. And, there are potentially more input checks that would have to be done in a more strict way than before.
Here is the result:
CPU cycles and round-trip time that the ZeroTier overlay adds to one ICMP echo, new client against the ported reference, same board, same network, same peers. One pass of 1,000 echoes for each point; no error bars yet.
Here comes the surprise: On the same board the new client spends about a third of the cycles of the reference for one echo and requires only 1/38 of the original code (11,692 bytes against 448,928) and 1/5.7 of the RAM (20,212 bytes against 115,052). So, approx 3x faster. Wow.
Moreover, in a one-hour run it answered 360,000 of 360,000 echoes, losing zero (previous implementations would lose some due to timeouts or overload).
Having said that, I do admit that the two versions (reference and new) do not do the same work: the reference also holds the parts that a leaf does not need, and it uses AES where the new client uses the older Salsa20/12 suite. However, ultimately, that is the point of a rebuild: the contract says what is needed, and the rest is just not there.
Limits
"Proved" means that the code meets its written contract, in the tools' model of C. A person wrote the contracts. The compiler is trusted. And some things are not yet proved at all: - that a "yes" of the authentication means a correct code - only the test vectors from the reference show it, but that suffers from the same "maybe there exists an instance that causes error" problem - protection against replayed packets (the protocol has none); - timing.
The client, by design, has no AES and does not check the controller's signature. The new code lists 38 such points.
One more lesson came on the way. A change of solver version lost three proofs that the older version had found; A proof is a result of code, contract and tools. Hence, from now on, tool versions are pinned, and the whole run repeats after every upgrade.
Evidence: zerotier-leaf-c, state of 14 November 2026: proof totals from one full run of the runner (Frama-C 33.0, Alt-Ergo 2.6.4, Z3 4.13.3, CVC5 1.3.2, CBMC 6.6.0); deliberate errors from one run of the whole list; sizes and cycles measured on one Teensy 4.1 (Zephyr 4.4.2, -Os), one pass of 1,000 echoes for each payload size, taken before the last change of the code (about 120 bytes of code more since). Methods and all tables: the full report.
Next: more kinds of proofs, more tools
The proofs above are about one call of the client that nothing interrupts. Around the client is an adapter for the operating system, with two threads and one mutex, and those proofs say nothing about it.
The tool for that part is VeriFast, a verifier built on separation logic. In separation logic a function must own the memory that it touches, very much like what Rust does, but applicable to C by means of annotations.
So VeriFast can be used to prove what the C itself does not state, without the need to infer it back: that a thread touches the client's state only while it holds the lock, and that each buffer has exactly one owner at any time.
Next thing I want to check is, does this already-checked code, by chance is compliant with MISRA-C. Or maybe MISRA-C suggests something even more strict. Or maybe it can be proven that it requires too much. This is to be seen.
The point is that it has became amazingly cheap to apply all these checks at implementation time.
The code and all reports are public: github: source code : zerotier-leaf-c. The full report has the method, the tables, the failures and the limits.