Rebuild from a contract: full report on the proved ZeroTier leaf
This report belongs to the post "Bugs? Rebuild it from a contract. Case study." The source of every number is the public repository zerotier-leaf-c, state of 14 November 2026. Its own reports go deeper than this page: PROOFS.md (every proof and every failed attempt), NOT_PROVEN.md (the review checklist), PERFORMANCE.md and the tutorial.
1. Background
ZeroTier. An overlay network. Each node has a 40-bit address and a key pair. Nodes exchange UDP datagrams (the underlay); inside each datagram is a packet with a 64-bit packet ID, destination, source, flags, an 8-byte authentication code and an encrypted payload, for example one Ethernet frame of the virtual network (the overlay). A packet longer than 1,432 bytes travels in two datagrams. A controller node hands out the network configuration.
Overlay and underlay (drawing from the repository's tutorial).
The leaf. A leaf talks to peers that it knows and relays for nobody. This leaf is narrower still: 7 peers, each pinned at build time with a shared key that a provisioning tool computes on a PC, and one network. So the device needs no public-key arithmetic. It announces protocol version 11, so stock peers use the Salsa20/12 and Poly1305 suite with it, not AES.
The reference. The core of ZeroTier One 1.16.2 (C++), ported to the same board as a Zephyr module. It gives the comparison for size and speed, and it produced the test vectors.
The tools. Frama-C WP reads a C function and its contract (written in the ACSL language in comments) and produces proof goals; automatic provers (Alt-Ergo, Z3, CVC5) must close each one. A proved goal holds for every input that the contract allows. WP works one function at a time: a caller is proved from the contracts of what it calls, not from their code. CBMC turns a whole program, with every loop unrolled to a bound, into one formula; it finds real counterexamples but only up to that bound. Frama-C Eva computes the possible values of every variable.
The path of one received datagram (drawing from the repository's tutorial). Each box is a function with a contract.
2. The method
The code is restricted so that the provers succeed:
| Rule | Why |
|---|---|
| No heap; all state in one structure of 7,136 bytes | Memory safety becomes a statement about fixed ranges |
| No recursion, no call through a pointer | Every call is known; each call uses the contract of exactly one function |
| Every loop has a written bound | Termination is a proof goal, not a hope |
| No arithmetic that wraps, no conversion that loses bits (unsigned included) | The provers reason about integers, not about bits; value statements become provable |
| Small functions | Each proof goal stays small; this is what made the cryptography provable |
| A contract on every function | The unit of proof, and the unit of review |
The work order was: contract first, code second, proof third, then a deliberate error for each rule (a wrong version of the code that the proof must reject). When a caller's proof failed, the usual repair was a stronger contract on the function that it calls.
3. What is proved
One full run of the runner (proofs/run.sh), all steps passed:
| Step | Result |
|---|---|
| WP, 64-bit model of C | 4,296 of 4,296 goals |
| WP, 32-bit model | 4,301 of 4,301 goals |
| Search for contradictory contracts and unreachable code ("smoke") | 1,065 tests, no finding |
| CBMC on the datagram classifier, 64-bit and 32-bit (ARM) | 0 of 470 and 0 of 471 checks failed; all 11 kinds of outcome reachable |
| CBMC on one Poly1305 step | 0 of 1,720 checks failed |
| Test vectors made by the reference | 725 inputs in six groups, 0 failed |
| Protocol test (300,000 random rounds, address sanitizer) | 1,681,597 checks, 0 failed |
| Deliberate errors | 104 errors, 118 tool runs, all rejected |
The statements, in plain words (the repository numbers them L-1 to L-32):
- For every function: no run-time error; no read or write outside the memory that the contract names; no wrap; every loop ends; the result meets the contract.
- Classifier: head, fragment or drop by the exact written rule, equal to a model of the reference for every datagram of 0 to 2,049 bytes.
- Reassembly: both orders of arrival give the head bytes and then the fragment bytes; nothing above 2,048 bytes.
- Authentication before effects: no frame for the host and no reply comes out without exactly one "yes" of the authentication, with the key of a pinned peer whose address is the source of the packet.
- One packet ID for each packet.
- Parse after build: what the leaf sends, its own receive path reads back with the same packet ID, destination and source; a packet in two datagrams comes back byte for byte.
- Cryptography: no limb of Poly1305 overflows for a message of any length; a refused packet is left unchanged.
4. What the method found
The repository keeps one paragraph for each place where a contract or a check became stronger (improvements-applied.md, 30 entries). A selection:
| Finding | Found by |
|---|---|
A node whose own address starts with 0xff sends heads that read as fragments; no precondition excluded it |
The round-trip proof (sender against receiver) |
| Three answer builders said nothing about the packet ID; a version with two IDs for one answer passed function by function | The caller's proof |
| The compiler replaced the wipe of key material with a library call and may delete it | The target build (provers read C, not machine code) |
| The dictionary reader passed all 144 vectors made by the reference's writer and still accepted a wrong line end; a writer never writes what it escapes | A deliberate error that survived |
| A defensive branch after the authentication call could never run; it would have stayed silent if wrong | The smoke step |
| The reassembly read a time stamp that was never written | A review by reading (for WP an unwritten integer is just some integer) |
None of these changes the protocol.
5. What failed
- CBMC on the whole reassembly at full packet size. The built-in SAT solver stopped at 78 GB (its own size limit); with two other solvers the formula passed 370 GB and was still growing. Consequence: small functions with contracts, proved with WP at full size; CBMC stays as a cross-check at 40 and 64 bytes.
- Solver upgrade. The move to newer solver versions (Z3 4.13.3, CVC5 1.3.2) lost three goals of the last Poly1305 step. No prover closed two of them in 300 s. The repair was two assertions that state the two cases of a constant-time selection, so that each case is linear arithmetic. Lesson: pin the versions; repeat the whole run after each upgrade.
- Index shifts and bit arithmetic. A statement over "byte j" against "byte 1,432 + j" defeated the provers until it was stated in two halves. A flags byte written with
|defeated them until it was written as one of four constants. - A harness that was partly empty. The smoke step reported unreachable code in a proof harness that I had written an hour before: a helper had a branch that the case under proof never takes.
6. Size and speed
Board: Teensy 4.1 (NXP i.MX RT1062, Cortex-M7 at 600 MHz, code runs from flash), Zephyr 4.4.2, -Os, member of a ZeroTier network with a stock 1.16.2 controller and stock 1.16.2 peers. The underlay is the board's USB network link.
| This leaf | Reference | Ratio | |
|---|---|---|---|
| Code added to the application | 11,692 bytes | 448,928 bytes | 1/38 |
| RAM added | 20,212 bytes | 115,052 bytes | 1/5.7 |
| Cycles added to one echo, 16-byte payload | 498,892 | 1,569,027 | 1/3.1 |
| Cycles added to one echo, 1,252-byte payload | 784,717 | 2,023,955 | 1/2.6 |
Method for the cycles: an ICMP echo to the overlay address and the same echo to the underlay address, 1,000 for each payload size, 100 each second; the cycle totals of all threads are read before and after; "added" is overlay minus underlay. One pass; a repeat with error bars is to do. At 500 echoes each second the reference is saturated on this board, so the comparison is at 100.
Inside the leaf, one received frame costs 45,000 to 113,000 cycles and one sent frame 30,000 to 97,000 (16 to 1,252 payload bytes; average of 3,000 echoes): about 55 cycles for each byte in each direction. Most of the added cycles are outside the leaf, in the adapter, the UDP socket and the second pass through the network stack.
One-hour run: 360,000 echoes of 1,252 bytes, 100 each second, 360,000 answered; round trip 2.81 ms on average, 11.5 ms at most.
The call graph is fixed (no recursion, no pointer calls), so the stack has a bound that a script computes from the compiler's own figures: 536 bytes for the deepest path of the receive call.
Static call graph of the nine source files, from the compiler (tools/callgraph/callgraph.py in the repository). Blue: protocol; orange: receive gate; violet: cryptography; green: decoders.
7. Limits
- A contract is written by a person. The deliberate errors and the smoke step guard against contracts that say too little; they do not prove that a contract is the right one.
- The provers work on a model of C. A read of memory that was never written, pointer alignment and the compiled code are outside it. The compiler and the hardware are trusted.
- Not proved, tested with vectors from the reference: that the authentication answers "yes" only for a correct code; Salsa20/12 and Poly1305 as whole functions; which malformed messages are refused.
- Not there: protection against replayed packets (protocol version 1 has none; the reference limits the rate of some answers), AES, a check of the controller's signature, evaluation of network rules, more than one network.
- No statement about timing. Constant time is by construction and by reading the compiled code.
- The Zephyr adapter (sockets, threads, one mutex) has no proof and no test of its own beyond the runs on the board.
- The measurements are from one board and one pass, taken before the last change of the code (the header of a packet is now written in one place; about 120 bytes of code more).
8. Cost
One full proof run: about 32 minutes on a 32-core machine, memory peak 5 GB. The whole list of deliberate errors: about 2 hours more. Tool versions are pinned in the repository (Frama-C 33.0, Alt-Ergo 2.6.4, Why3 1.8.2, Z3 4.13.3, CVC5 1.3.2, CBMC 6.6.0).