Some of the checks a verifier runs are written down twice: once as code, and once as a model, a small description of the rules in a language called Lean. Lean is a proof assistant. A proof is an argument Lean checks step by step, so a proved statement cannot be wrong about the model, only about whether the model matches the world.

A model on its own guards nothing; the risk is in the gap between the model and the code. So each model here also writes the tests for the real code. The model computes the expected answer for every test case, the test runs the real verifier on a real input, and the two must agree. If anyone edits the model without regenerating the tests, the build fails.

Three terms come up below:

• A spec is the list of rules the model states, each as a numbered requirement such as "the verifier MUST refuse a receipt whose sandbox allows networking".
• MC/DC (modified condition/decision coverage) means every requirement is, in at least one test case, the only rule that is broken. That proves each check in the code is actually exercised and actually decides the answer.
• A mutant is a copy of the code with one deliberate bug. Running the tests against mutants measures whether they catch real mistakes.

Mac launch receipts

When an agent runs on a Mac node, the node starts it in a box: a launchd job with a Seatbelt sandbox. The node then signs a launch receipt saying how the box was built and what it read back from it. A verifier credits the receipt only if every rule holds: the box is the published one, the job is that box's own, only the node can start it, the node itself read the sandbox and found networking and the protected paths denied, the agent runs as its own non-root user, and the receipt does not claim more coverage than it has.

What is guaranteed. The model proves that a receipt is credited exactly when every one of its requirements holds. It also proves something about which process the sandbox reading is about. On a Mac, the launchd job's own process is the observer that watches the agent, not the agent, and it runs unsandboxed. The receipt therefore carries the agent's process id separately, and the model proves a credited receipt's sandbox reading always names the agent and never the observer.

How it reaches the code. The model writes 1,893 test cases. Each changes one or two fields of a valid receipt (every value of every field, and every pair of fields), signs it, and runs the real verifier, checking exactly which rows refuse it. Every requirement is the sole cause of a refusal in at least one case, except two that another requirement always reports alongside.

A worked example. Case agentPid=4242+sbPid=4242 is a receipt whose job is process 4242, and which says the agent is also 4242 and that the sandbox was read on 4242. Everything else is valid. It is refused under the job row (B4), because the "agent" it names is the observer. That is the case that proves the observer rule is checked on its own: no other rule is broken.

What is not covered.

• Lineage. The rules also require the agent to be a descendant of the observer, as Endpoint Security saw it. No receipt field records that today, so no verifier can check it, and the model proves the verifier credits a receipt whose agent is not a descendant. The tests for that case are marked as expected failures until the field exists. Until then, no Mac receipt is credited at all.
• Order. The sandbox must be applied before the agent says hello. No field records the order.
• The rows Linux shares (the signature, the node's registration, the session key, the receipt time) are held at valid values, not varied.
• Which reason. The tests check which row refuses, not the wording.
• The node's own checks before it signs are not modelled.

When the tests were first run, an independent reviewer wrote 12 mutants without seeing them. The tests caught 10. The two misses were fields the model lacked (a source string that looks like the node's, and a root agent); both fields were added, and the extended tests catch all 12.

For the full list of requirements, each tied to its proof, its test case and the code it constrains, see the generated specification, SPEC.md, in the formal/receipt-v5 directory of the source repository.

The Linux fanotify tracer never stalls the build

On Linux, cilock can watch a build's file reads with fanotify. For each file the build opens, the kernel pauses the build's open() and asks cilock for permission; cilock reads the file, records its digest, and answers "allow". The kernel never gives up waiting on its own, so a question cilock never answers stops the build for good.

What is guaranteed. For every kind of event cilock can be handed, the model proves that a permission question is answered exactly once and as the last thing cilock does with it; that a plain notification is never answered; that nothing before the answer can take unbounded time (reading the file has a time limit, and the answer goes out even when the read never finishes); that cilock's own file opens are answered without touching any file, so cilock never waits on itself; and that cilock never reads a file it must not, such as another program's or a pipe, which would steal the pipe's data or hang.

How it reaches the code. The model lists every combination of the nine facts the code decides on, 3,072 of them, and proves the list is complete. It writes one test case per combination. Each case builds a real event and runs the real handler, then checks how many answers it wrote, whether it read the file, and how long it took.

A worked example. Case self=true+file=fifo is a permission question about a pipe, asked by cilock's own process. The expected result is one answer and no read: the model's rule is that cilock answers its own questions without touching the file, and never reads a pipe.

What is not covered.

• Facts taken as given. How the kernel and Go's runtime behave, and that looking up a file's metadata returns promptly. That last one is false on a stalled network filesystem.
• Getting the question to cilock. If the part of cilock that collects the questions stops, nothing answers them. That is the next part of the model, and it found a bug the code is being fixed for.
• Whether every read ends up in the attestation with the right digest. That is a separate model, still to come, as are the other two Linux tracers.