What is proven,
and what is enforced

01The problem it retires

In compartmented environments one engineer is routinely cleared into several programs at once. The common workaround is one account per compartment: separate logins, separate desktops, separate credentials, and a human keeping them apart. That arrangement is expensive, it puts the isolation property in the operator's discipline rather than in the system, and it fails at exactly the moment it matters most, which is de-accession. Disabling an account does not touch labelled bytes already on a shared workstation.

n0de takes the other route. Authority derives from current attributes and nothing else, and every access is decided against them. One identity carries ALP and BRA at the same time and reads both. A compartment the identity does not hold is not merely denied, it is invisible: objects in it do not appear, and their existence does not leak through a name collision. De-accession is one attribute change, after which every object carrying that compartment is denied on the next decision, residue on the machine included.

The system runs on ordinary open components. Lean 4.31.0 with mathlib for the proof, Cedar 4.11.2 for the policy decision point, PostgreSQL 18 with row-level security for the store, Node 22 using only its standard library for the identity and file API, and SELinux MCS as the operating-system reference monitor, on Fedora.

02The label, and the one decision function

A label has four axes: level, compartments, need-to-know, and releasability. Levels and compartments map onto SELinux MLS sensitivity and categories. Need-to-know is a first-class dimension rather than a convention. Releasability is the set of countries an object may be released to, with NOFORN being the singleton set containing the United States, and each subject carrying a citizenship. Dominance over that axis is reversed set inclusion, so a narrower release is more restrictive.

Those four axes form a lattice, and dominance over the lattice is the whole of the read rule: a read is permitted when the subject's effective label dominates the object's on all four axes at once. A write must dominate in the other direction, which is the Bell-LaPadula star-property, and it may not widen releasability. Both directions are theorems rather than code review notes: read_permit_sound and write_permit_sound, with transfer_deny recording that the decision point never authorizes a cross-domain transfer at all.

There is one proven decision function, decide, defined in the Lean model. There are then several independent implementations of that policy in the running system: the Cedar policy set, the Postgres row predicates, and the JavaScript decision mirror in the API. They can drift, which is the entire reason the gates exist. Each is differentially checked to agree with decide rather than assumed to encode it, and the same compiled proof function is available as a command-line oracle, so the running engine's verdict can be put beside the proven one on any input.

The distributed agent is a different case and is worth separating, since it is easy to read the gate list as one long equivalence check. The agent's decision path reduces to the same function, but most of the gates around it are operational rather than decision-equivalence tests: they exercise fail-closed behaviour on partition, replication, key handling, revocation, failover and clock trust. Those are properties of the deployment, checked by running it, not statements derived from the model.

03What is proven

The theorems live in model/Pl4Abac/. The keystone is Pl4Abac.noninterference: writes by a high or foreign-compartment subject never change what a low observer sees. Because the label carries all four axes, that statement ranges over all four, including releasability.

Not the full index, and every name above appears verbatim in docs/THEOREMS.md, which maps each theorem to the attack it stops.

Two results worth reading together

naive_create_leaks and poly_create_ni are a pair, and the first is the unusual one. Rather than assuming the existence channel is a problem, the model proves that a shared namespace leaks the existence of an object a subject may not read, then proves that polyinstantiation closes it. Stating the attack as a theorem is what makes the fix checkable rather than asserted.

The de-accession group is the other one. Three separate statements are needed because a single-step result is not the property anyone actually wants: deaccess_revokes_read covers the next decision, deaccess_residue_invisible covers bytes already on the machine, and temporal_deaccess_blind covers arbitrary traces, so blindness is not a claim about one moment. revoked_then_blind then says it persists until an explicit re-grant, which is what stops a re-accession race from quietly restoring access.

Axiom footprint

04Proven, then pinned

A proof of a policy says nothing about the code that runs. The bridge is engine/ci.sh, which re-runs every differential gate that pins an enforcement layer to the model and prints one verdict. It builds the Lean oracle and the Cedar policy decision point first, then runs each gate under a 180 second timeout, standing up an ephemeral Postgres where a gate needs one.

There are 42 gate invocations. One is a regression gate over known attacks; the other 41 are the E-numbered gates, which carry labels E1 through E41 because E4 and E5 share a line, E24 is unassigned, and E29 and E34 each run as two lines. The full inventory, read out of the file:

Read directly from engine/ci.sh. Each row names a script in the repository, so the mapping from claim to executable check is one file lookup rather than a matter of trust. Three lines need a real cloud account (E31, the live half of E34, and E39); without it the script reports them as skipped, and it says in its own summary that a skip is not a pass.

Two of these deserve their own sentence. E22 exists because a differential harness can be fooled by its own oracle: the Lean oracle's string parsing silently coerced an out-of-domain field rather than failing, which would have let a differential run compare a verdict on an input neither side actually received. A gate that checks the gate is the unglamorous kind of assurance work that only gets written after somebody looks for it. E21 fuzzes the JavaScript decision mirror against decide over 8,000 cases, because the mirror is the piece most likely to drift and least likely to be noticed when it does.

The kernel gate runs separately, and its scope is narrower

The SELinux differential is not part of ci.sh. It lives in reality/ and is run on its own, because it needs a live kernel with the right policy loaded rather than an ephemeral container. It queries the loaded policy through libselinux for a constrained domain pair, which computes the real kernel access decision including the MCS constraint.

The recorded run is 2026-06-29, on Fedora with the targeted policy, enforcing, MLS enabled: 8 cases, model and kernel agree on all 8. The repository is explicit about what that does not cover, and so is this page. It exercises categories, which are our compartments, and not the sensitivity hierarchy, because the targeted policy fixes sensitivity at s0. It covers the read direction only; the star-property is proven in Lean but was not differentially tested against the kernel. And it is valid only for confined domains, since unconfined_t is exempt from MCS and reads across categories freely, which was observed directly rather than assumed.

05The distributed increment

The single-host arrangement assumes the decision point is reachable. The distributed layer answers the harder question: what does a machine do when it is offline, stolen, or has just been de-accessed and does not know it yet.

An authority mints short-lived signed leases carrying a subject's attributes. A local agent serves reads from its own replica and enforces them against the held lease, contacting the authority only on the renew tick. When it cannot renew, because the network is partitioned or because the authority has revoked the principal, the lease passes its expiry and the agent denies unconditionally. The exposure window is bounded by the lease TTL, and there is no path in the state machine that opens access without a fresh valid lease.

Three theorems in Lease.lean state exactly that. lease_expired_denies is the decision form: once the lease has expired, every access is denied, any object, any action, without consulting the policy at all. lease_expired_blind is the observation form: the agent sees nothing, residue on the box included. lease_revoked_blind is bounded-staleness revocation: once the renewed lease no longer carries a compartment, the agent is blind to every object carrying it, whether or not the lease is currently valid.

The aggregation gate crosses the same boundary the same way. Knowledge and the compilation rules ride in the signed lease, so the offline agent enforces the gate against the authority's last-known view plus what this machine has itself absorbed - recorded durably before delivery, reported upstream on renew, carried back in the next lease. A stale snapshot is proven never to over-deny (stale_knowledge_never_overdenies); the exposure direction, a tipping fact delivered inside one TTL of a cross-channel absorption, is the same bounded-staleness statement as revocation, and E28 exercises the whole loop including a wiped machine inheriting suppression from the lease alone.

Around that core the gates cover the operational failures rather than the policy ones: content encrypted at rest under per-object keys that the agent holds only in memory (E12), signed revocation as a hard kill that latches until restart (E13), key rotation by epoch (E14), authority replicas with agent failover (E15), Postgres streaming replication with failover (E16), and synchronous replication so that a confirmed de-access survives an instantaneous primary loss with zero RPO (E17). E18 covers clock trust, using a monotonic clock and anti-replay so that moving the wall clock backwards does not resurrect an expired lease.

The cross-domain increment

Release across domains is the one place the model lets information flow down, and it does so only through a guard. only_authorized_flows already said that a guarded run is low-equivalent to running only its authorized releases, with the authorization bit as an input. The increment replaced that input with a predicate. The engine's release check is five steps over an ECDSA-signed verdict tuple, and Verdict.lean states those steps as the predicate verdictOk, with the signature result as the one input that remains: verdictOk_binds says a passing verdict is bound to its request on every identifying field and carries an output label under the destination ceiling, authorized_within_ceiling says a guard cannot lift that ceiling, and verdict_flows composes with the intransitive result so that a low observer's view depends only on verdict-authorized, ceiling-bounded releases. E35 pins the engine's check to the predicate over 5,000 real-signature cases, E33 attacks it, and E32 and E34 run the release path end to end.

Around the guard, three further increments are pinned rather than proven. Identity: a real OpenID Connect provider verifies tokens and syncs claims into principals, so officer actions attribute to a named human (E36 to E38). Ingest: a destination authorizes delivery solely on the guard's signed verdict, verified against a key it registered itself, so the ingest credential authenticates and authorizes nothing (E40), and concurrent retries of one release land exactly once (E41). Storage: labels become S3 object keys and a bucket policy generated from the label universes makes S3 itself return the proven read verdict; the real account is the gate that earns the word enforced (E31), and the two offline lines (E29, E30) check the codec and the adapter.

06What is not claimed

This is the section that makes the rest of the page worth reading. What is proven is the confidentiality decision logic over all four label axes, including releasability, plus its refinement to the row-level-security predicate, plus kernel agreement on the compartment dimension. The disclosed frontiers, stated as the repository states them and not softened here:

• The trusted-desktop surface. Display, clipboard, peripherals and timing channels are outside the single-machine model. This is where a trusted access tier belongs; the access layer is pluggable, with a no-op provider and a Kasm provider, and the gate for it (E9) runs offline.
• Object and exhaust labelling. The decision point governs known objects, not the per-artifact exhaust a workstation produces: temp files, swap, logs, clipboard, print, network. Enforcing at the application layer while exhaust lands on unlabelled storage is a spill path around the proof. Closing it needs born-labelled artifacts under SELinux MLS with single-label confined sessions, encrypted swap and labelled networking. The data tier itself is already ciphertext at rest. This one is worth reading against the residue claim in section 01: a de-accessed subject is provably blind to labelled residue, and that says nothing about bytes which were never labelled.
• Label reclassification, and label origination generally: the first marking of a new document is a human legal act, out of scope by design.
• Aggregation and inference - split, because half of it moved. The rule-based half, classification by compilation, is no longer a frontier: objects carry content facets, compilation rules elevate combinations, each subject's absorbed facets persist, and a read that would complete a compilation above the subject's label is suppressed - absent from the response, indistinguishable from ordinary non-visibility. That is proven (naive_compilation_leaks, agg_knowledge_bounded, agg_no_tipping_delivery) and enforced through the running API, pinned by gates E25-E27. The suppression itself is proven silent for the subject's own view: a suppressed object contributes exactly what a nonexistent one does (suppress_eq_absent), and the alternative - a visible deny - is proven to be an aggregation oracle (marked_deny_leaks), which is why the engine ships silence. What remains unclaimed: statistical inference with no written rule, and the fidelity of rule and facet authoring: the guard is exactly as good as the guide it encodes.
• Coalitions - proven in the model, not enforced. Two subjects each below every trigger, pooling what they read outside the system, defeat the per-subject gate. A coalition gate now exists in Coalition.lean and CoalitionObs.lean: a coalition's joint authorization is the meet of its members' labels, so a compilation is authorized only if every member may hold it (le_jointAuth_iff); no trace of reads by anyone lets a declared coalition exceed it (coalRun_inv); and what denial reveals is stated rather than hoped - a coalition-mate's read can flip a verdict (coalition_reads_interfere), after which the verdict for that subject and object is constant over time (deny_forever) and never depends on content (verdicts_independent_of_content). None of it runs: there is no engine mirror and no gate, and this page's rule is that a claim means proven and enforced. Until it ships, the running engine controls compilation by a subject, not by a conspiracy, and comparing views out of band remains the only way to observe a suppression. Open on the model side: a bound on what denial bits reveal across many objects, locality across overlapping coalitions, and the over-denial cost of the meet measured on real rule sets.
• Attribute-source integrity. The proof assumes the attributes are honest. It does not verify the pipeline that sets a person's clearance or compartments.
• De-access TOCTOU and replay at the boundaries of the enforcement path.
• Full mechanized refinement to SQL and OS semantics. What exists is predicate-level refinement, which is a weaker statement than a mechanized model of the database.
• Dual citizenship and per-session releasability contexts. Multi-country REL TO objects are seeded-only in v1. Authoring them is the foreign-disclosure-officer increment, and it is not built.

Two further limits worth naming in the same breath. The kernel differential covers the compartment dimension, so full sensitivity-hierarchy enforcement end to end is not demonstrated against a live kernel, and closing it needs an MLS-policy host rather than new research. And timing, termination and probabilistic covert channels need a quantitative model, which this is not.

Separately from the proof: an implementation security review answers a different question from the gates, which is whether anything can get around the enforcement rather than whether the enforcement matches the policy. That review found no injection or authentication bypass and hardened three defense-in-depth gaps, and empirical probing found one real existence leak through a duplicate-key status oracle on the write path, since fixed by masking with a regression added under E7. A full external penetration test against a real deployment is still owed and is not substituted for by any of this.

07Check it rather than believe it

Everything above is re-runnable by someone with the repository in front of them. The proof rebuilds and kernel-checks with lake build, and model/check.sh scans for admitted goals and prints the axiom footprint of the headline theorems. The pinning suite is engine/ci.sh, one command, one verdict, ephemeral Postgres per gate as required.

The demo is the same check made interactive: an engineer workspace where one identity spans two compartments and a third stays invisible, a security console that grants and de-accesses live, and a decision probe where a reader types a hostile case and sees the running engine's verdict beside the verdict of the compiled Lean oracle on that same case.

Being exact about what that comparison shows, because it is the point where a demo invites the wrong conclusion. A theorem does not agree or disagree with a case; it is a universally quantified statement, already checked by the Lean kernel, that no input can exercise. What the probe compares is two executions, the engine's and the compiled oracle's, and what it detects is drift between the implementation and the proven function. The theorem is named alongside because it is the property that function was proven to have. Agreement on a case is evidence the implementation tracks the model; the guarantee itself comes from the proof, not from the case.

The releasability case is the one worth trying first: a foreign liaison reading a NOFORN object is denied, and the same read against an object marked REL TO that liaison's country is permitted.

The repository is private today, so this is what an evaluator with access runs rather than something a reader can clone from this page. The demo is one command and about ten seconds to a browser, and it is available on request.