Evidence

Three different kinds of evidence stand behind this site, and they are not interchangeable. A measurement on a live kernel is the strongest; a model checked against the kernel source is weaker; an SMT proof about a hand-written model is weaker still. Each claim below says which kind it is.

1 · Measured on a live kernel

Linux 6.1, CONFIG_BPF_LSM=y, blocking mode, the 2026-08-07 build. Source of truth: the project's claim ledger. Nothing that is not in the ledger with a status is claimed here.

D-16–D-20 were measured on 2026-09-11 on the disposable VM in blocking mode, with a real token minted to the probe. What was measured is the effect — the write() allowed or refused — with two differential controls (the same file under a WRITE vs a NET token; the same token on an unprotected vs an OP_BLOCK file), so no result is explained by a missing token. The kernel's verdict names were not captured in that run, so this is one step short of the T08-level corroboration; a re-run that records them is still owed.

Open obstacles

• O-D3 — nothing is deployed; the long-running host still runs an older build in log-only mode.
• O-D4 — the shared secret used to authenticate token requests is protected only by file permissions.
• O-D5 — read mediation, measured on the older build in May, did not reproduce on the 2026-08-07 build; the cause is not yet known.

The token-dependent paths — now measured with a real token

These paths need a process that holds a valid token. Until the authority existed (2026-08-07) no token was ever created on the test machines — the key-press source never attached — so every such test blocked for the trivial reason that there was no token. The project's 2026-08-07 summary withdrew those as evidence. On 2026-09-11 they were re-measured on the disposable VM in blocking mode, minting a real token to the probe (D-16 – D-20): the TOCTOU pivot, the multi-write to the bound inode, op_class against an axiom, an OP_BLOCK file with a live token, and fork inheritance all gave the expected allow/refuse. The discrimination is carried by two differential controls — the same file under a WRITE vs a NET token, and the same token on an unprotected vs an OP_BLOCK file — so none of the results is explained by a missing token.

What is still owed: that run captured the effect (the write() allowed or refused), not the kernel's verdict names, whose audit stream produced no journald lines. And content binding (D-11) remains planned — a token authorises writing a file, not writing a particular content.

Earlier results (2026-05-25, validation report v1.4)

On the long-running host, in blocking mode: T01 (a write with no token) was refused with EPERM, and T10 (writing the token map from user space) was refused even for root, because the map is frozen. The report also lists T03 (protected file) and T04 (op_class mismatch) as blocked; by the reasoning above those two results cannot tell a working rule from a missing token, and are not relied on here. T13 (root rewrites the axiom map) succeeded, as documented: a software layer does not stop root. The report's T08 result is superseded — see below.

When only a physical button can open the window

The design goal is that nothing outside the scope runs unless a person physically acts. Writing that rule down does not make it hold; where it is checked decides who can go around it. A check inside an agent can be bypassed by a child process the check never sees; a check in a service can be bypassed by not calling the service. A check in the kernel sees every process. Five conditions must hold together — two of them do not yet:

With condition 2 met by a hardware key whose touch signs the specific request, and condition 5 by content binding, the rule becomes one that a process on the machine cannot go around. Against root, the check has to move lower still — a hypervisor or hardware.

2 · The emulator against the kernel source

The emulator on the main page is a model of dcc_core.bpf.c as built on 2026-08-07. It is checked in three ways:

• 36 conformance tests, each naming the kernel lines it pins: window length and boundary, which hook consumes a token, same-inode multi-write, TOCTOU rollback, fork inheritance, whitelist precedence, the axiom key, guard defaults, log-only mode, exit cleanup, the stop path.
• A source pin. If the kernel source changes in any of the ways the model depends on — the window constant, the fork rule, the number of programs (22, of which 18 are LSM hooks) — a test fails and names what changed.
• Mutation testing. 23 deliberately wrong versions — 20 of the model, 3 of the source — are run against the suite. All 23 are caught.

This establishes that the model follows the source. It does not establish that the kernel behaves like the source says; that is what section 1 is for.

3 · The Z3 model

The check this site used to cite proved nothing

Until 2026-09-11 this page showed “6/6 invariants formally verified” and “isomorphism proven”. Each of the six checks added a rule of the form A implies B and then asked Z3 whether A and not B could hold. That combination is impossible for any A and B, so the check passes whatever the kernel does — with the error code set to a nonsensical value it still printed the same result. It has been withdrawn.

What replaces it

The write-path decision — the program on lsm/file_permission together with its axiom and token checks — is written out as one Z3 formula over all of its inputs, following the kernel source. Z3 proves 9 properties of it for every input, among them: an ordinary writer gets through only with a live token; an expired token never does; an OP_BLOCK file is refused to everyone but the loader, whitelist included; a second file with a bound token is always refused, even in log-only mode; every refusal is EPERM; and a whitelisted writer passes every other file without a token. Each property is also checked the other way: its premise can occur (it is not true merely because nothing satisfies it), and removing the one guard it depends on produces a counterexample.

The formula and the emulator are then run on the same 896 input combinations; they agree on all of them. Together with the conformance tests this is a chain — kernel source → emulator → formula → properties — but every link is a model. None of it is a measurement of the running kernel; section 1 is.

The invariants as they were published

Besides being unproven, several of the six published invariants said things the kernel does not do:

The earlier page also attributed these invariants to three BPF programs — dcc_token_validator, dcc_toctou_guard, dcc_scope_checker — that do not exist. The checks live in dcc_axiom_validator, dcc_network_guard and the other programs named on this site.

4 · Changes since the papers (2026-05-25)

• Name-spoofing (T08). The May report recorded the spoof as blocked. The August measurement shows it succeeds against a name-keyed whitelist (D-12). The fix binds identity to the executable file, and that is now PROVEN (D-15).
• PID recycling (T09). A recycled process ID could inherit a dead process's token or identity. An exit hook now clears both (ledger O-D7, O-D8, fixed and measured).
• Token source. The key-press tracepoint is absent on the 6.1 generic kernel (O-D1). Tokens now come from an authority that only a privileged caller can run, reached through an authenticated request (D-05 – D-07).
• Coverage. On the older build, 2 of 13 ordinary file-modifying operations reached the hook. With 11 new LSM hooks, 16 of 17 do (D-03). UDP egress is mediated (D-04).
• Stopping. The operator can stop the layer without a reboot (D-08); an earlier hang in that path was found and fixed, then measured over three consecutive clean stops (O-D9). An unprivileged process cannot stop the layer (D-09).
• Root sub-boundary. A user-namespace root cannot read or rewrite the maps, and unprivileged BPF is disabled, so there is no unprivileged path to the verifier. Both closures come from the kernel's own configuration, not from DCC.

5 · Limits

• Root can switch the layer off (D-13).
• A whitelisted binary passes every guard without a token; only an OP_BLOCK file still stops it. See Headless workloads.
• The file axiom is keyed on the first 15 characters of the file name, not on its path.
• Nothing is deployed (O-D3); all 2026-08-07 results come from one disposable VM.

Kernel model: dcc_core.bpf.c, build 2026-08-07. Ledger statuses as of 2026-09-11. The implementation source is not public; the technical dossier is available under NDA — admin@metaspace.bio.