The Verification Ladder

Design note. Snapshot against HEAD = 936e994 (2026-06-24). Citations are file + symbol where load-bearing; bare file:line numbers are as-of this commit and will drift on the shared trunk — chase the symbol, not the line. The companion epic roadmap is verification-ladder-epics.md; every epic there was adversarially citation-checked (a skeptic opened each cited file) and the four with line drift were corrected before landing.

The thesis

Verification should be flexible and granular. By default it should pick the smallest rung that can establish the property at hand, and climb to a costlier rung only when the cheap one comes back INDETERMINATE or the risk warrants paying more. This is the agent-kernel restatement of five things Linux already does: seccomp’s most-restrictive-wins return fold, the decomposition of root into least-privilege capability sets, AppArmor’s complain-then-enforce rollout, the integrity granularity ladder, and the eBPF verifier’s “prove the program cheaply before you admit it.”

The one observation that means we are half done

The load-bearing fact is already in the code: the adjudicator chain is cost-ordered and folded by a restrictiveness lattice. The authoritative reference monitor registers itself at rank 100 so cheaper pre-flight rungs run first (internal/adjudicator/decide.go:16-18, decide.go:671), and the kernel folds the chain by taking the most-restrictive non-Defer verdict by FoldRank (internal/kernel/kernel.go:178-199, lattice in internal/abi/registry.go FoldRank). Inside a single Adjudicate the rungs are evaluated cheapest-first and each early-returns on the first provable refusal (decide.go:255-374).

So “smallest rung that can work” is already half-built. What is missing is the other half, and it is three concrete things:

1. Short-circuit / lazy escalation. The kernel Fold runs the whole chain even after a maximal Deny is already seen — the loop at kernel.go:185-194 has no early break. It is order-independent (correct) but pays O(full-chain) where it could stop at the first conclusive rung. The per-call short-circuit exists (decide.go:255-374); the chain-level one does not.
2. A first-class INDETERMINATE verdict. Today a cheap rung either denies, allows, transforms, or Defers (abstains). Defer means “I have no opinion, ask the next rung,” and an all-Defer chain fails closed to DEFAULT_DENY (kernel.go:195-197). There is no verdict that means “I could not conclusively decide this cheaply, so a costlier rung MUST be consulted before we commit” — distinct from both fail-open and fail-closed.
3. Per-claim rung selection by risk. The per-call rung order is hard-coded in decide.go, not data-driven; you cannot say “this low-risk read needs only the name rung” vs “this write into a shared tree needs the arg-predicate plus the lint rung.” Every call that reaches a rung pays it.

This doc names the ladder, maps it onto the Linux primitives, draws the honesty boundary, reconciles it against what already shipped, and proposes the epics that build the missing half — each defaulting to the smallest sufficient rung.

The verification ladder

Rungs are ordered cheapest to costliest. The discipline is: start at the lowest rung that could conclusively establish the property; climb only when the rung is INDETERMINATE for this claim, or the risk warrants the next rung’s cost.

#	Rung	Cost	Conclusively establishes	Cannot establish (so you climb)	Exists today
0	vDSO / cache re-output	ns, in-proc	This exact call was answered before and the answer is reproducible	Anything about a novel call; it returns a blanket Allow with no adjudication	built — internal/kernel/kernel.go:303-314 (consulted before the fold; returns Allow by "vdso")
1	In-process structural adjudication (name / self-modify / arg-predicate / lint fold)	ns–µs, in-proc	A provable refusal (deny-map, SELF_MODIFY glob, arg-predicate violation, MALFORMED parse) or an affirmative allow	Whether a claimed effect actually happened; semantic safety of content; cross-process state	built — decide.go:255-374; folded by kernel.go:178-199
2	Posture / complain-mode admit-and-log	ns–µs, in-proc	That a low-risk read-shaped default-deny is safe to admit while recording a would_deny forensic record	Anything write-shaped or self-modify (correctly still fails closed); per-tool granularity	partial — decide.go:74-87, decide.go:377-389 (global per-policy binary, read-prefix-only)
3	Require-witness handback (corroborate a claimed git/object effect before dispatch)	ns–µs decide + one out-of-band resolver	That an agent’s claimed effect (“ancestor:HEAD”, “clean:.”) is corroborated by evidence it did not author	A quorum of corroborators; “evidence pending, retry later”; partial confirmation	built (binary) — internal/kernel/kernel.go:201-231; ship rung internal/shipgate/adjudicate.go:51-65 (rank 40)
4	CI suite (go build + vet + test)	seconds, local	That the change does not break the in-repo behavior on a clean tree	That the change is a gain; that main’s history corroborates the ship; cross-machine reproducibility	built — make ci / scripts/ci.ps1; the RSI track gate re-measures it (internal/rsiloop)
5	Git-evidence (dos verify)	seconds, reads git	That a claim landed from committed history rather than a worker’s self-report	That the change improved a measured metric; that it is reproducible off a clean worktree	built — dos verify (MCP dos_verify); the TruthClean bit feeds the keep-bit (internal/shipgate/shipgate.go:51)
6	Isolated-worktree measure (shipgate keep-bit)	ms-spawn + suite, off-main	That a candidate strictly improved a measured metric AND the suite is green AND truth is clean — non-forgeably	Whether a human should approve a dangerous-but-improving change; the smallest sufficient subset of the three	built (all-three) — shipgate.go:66-72 (improvedBit = improved() && SuiteGreen && TruthClean); worktree at shipgate.go:110-130
7	Human ESCALATE	minutes–hours	A judgment no rung below can make (risk, intent, policy exception)	n/a — terminal	built (only via breaker) — shipgate.go:95-105 (K consecutive non-keeps -> ESCALATE); routed via dos decisions

Two rungs sit beside this ladder rather than on it, because they are result-side rather than call-side: the context-MMU admit fold (screen/quarantine/page-out, internal/ctxmmu/mmu.go:136-218) and the recall re-screen on readmit (internal/recall/recall.go:344-396). They are the result-side dual of rungs 1–3 and share the same lattice (kernel.go:246-284), but the result-side fold is narrower — it acts only on Quarantine/Transform and silently admits a result-side Deny/RequireWitness (kernel.go:280-282). That asymmetry is a gap, not a feature.

Rosetta: the doctrine in five Linux mirrors

Linux primitive	Its graduated behavior	fak rung it maps to	The honest divergence
seccomp RET ladder + cross-filter fold (KILL > TRAP > ERRNO > USER_NOTIF > TRACE > LOG > ALLOW; kernel takes the most-severe return across all filters)	A severity-ordered disposition ladder, composed most-restrictive-wins, order-independent	FoldRank lattice Allow=0 < Defer=1 < Transform=2 < Quarantine=3 < RequireWitness=4 < Deny=100 (registry.go FoldRank), folded by kernel.go:178-199	seccomp keeps KILL/TRAP/ERRNO as distinct tiers; fak collapses every registered kind above the core into one fail-closed deny branch (kernel.go:352-363). fak has no soft mid-ladder ERRNO with a retry-after. Both lack chain short-circuit.
LSM stacking + POSIX capabilities (N modules each veto on the same hook; root decomposed into ~40 grantable bits; the bounding set caps what a child may inherit)	Authority is a least-privilege set; stacking only ever tightens; a child can never exceed the parent’s bounding set	DEFAULT_DENY allow-list (decide.go:363-389) + the adjudicator rank-chain as the LSM stack (kernel.go:148-153); arg-predicates as per-resource scopes (decide.go:54-117)	fak has the stack and the floor but no per-task bounding set: policy is one flat global object, there is no delegate-minus where a sub-step inherits a subset it can only shrink, and no no_new_privs-style monotone latch.
AppArmor complain -> enforce + the learning toolchain (per-profile permissive mode logs would-be denials; aa-logprof/audit2allow synthesize rules from the log; promote a profile to enforce once its log is clean)	Run permissive, observe what would deny, synthesize a rule, promote when proven safe	PostureAdmitAndLog + would_deny Meta (decide.go:377-389); the rulesynth Harvester/Detect/Propose/Validate learning loop (internal/rulesynth/rulesynth.go:126-202), folded into the keep-bit	fak’s complain mode is binary + global (one Posture enum on the whole policy, read-prefix-only). There is no per-tool complain dial and no promotion ledger that counts “tool X logged N clean would_deny events, therefore promote.”
Integrity granularity ladder (IMA/EVM measure at per-file vs per-block granularity; a Merkle tree lets you verify a subtree without rehashing the whole image)	Choose the integrity granularity that fits the object — a blob, a file, a tree	The content-addressed re-screen ladder: rung-0 verbatim digest (recall.go:349), per-page quarantine (recall.go:370-379), the CAS digest identity on every Ref (internal/abi/types.go:64-72)	Granularity is fixed by code path, not chosen by risk: every page-in re-screens every page unconditionally (recall.go:380-383); there is no “this blob is provably unchanged since its last clean screen, skip it” cheap rung, and no per-commit vs per-session vs per-blob selection.
eBPF verifier (a static proof that a loaded filter terminates, has bounded access, cannot crash the kernel — gates whether the filter may load at all)	Prove the verifier itself is cheap-and-safe before trusting it to run	Opt-in LintWrites parse-before-admit (decide.go:333-351, internal/adjudicator/lintwrites.go); architest’s TestHotPathHasNoExec; the non-forgeable improvedBit (shipgate.go:52)	LintWrites proves only Go/JSON syntax keyed off file extension, is off by default, and fails open (a quality gate). There is no structural admission check for a deployer-supplied rule (no RE2-backtracking guard, no “this rule would shadow the rank-100 self-modify floor” check).

Honesty boundary: structural vs heuristic, fail-open vs fail-closed

A rung is structural if its verdict is model-independent — it cannot be talked out of the answer by a cleverer prompt or a renamed argument. A rung is heuristic if it pattern-matches and is therefore evadable in principle. The discipline is blunt: a cheap rung that comes back INDETERMINATE must escalate, never silently allow.

Rung	Strength	Posture	Why
vDSO re-output (0)	structural-but-blanket	fail-open by design	A hit returns Allow with no adjudication (kernel.go:303-314); correctness rests entirely on FastPath.Lookup only hitting provably-safe calls. This is the one rung where a poisoned cache entry bypasses the whole lattice — flagged as the gap below.
name / self-modify / arg-predicate (1)	structural	fail-closed	Provable refusals: an exact deny-map hit, a glob containment failure, an arg-predicate violation. Unmatched falls to DEFAULT_DENY (decide.go:374).
SELF_MODIFY shell denylist	heuristic (substring, not a shell parser)	fail-closed, intentionally over-broad	Explicitly “intentionally over-broad” (command_writes.go:33-37); residuals like php -r are still uncaught (no php in interpreterEvalFlags, decide.go:491-496). A body that writes a guarded tree without naming it is invisible.
admit-and-log posture (2)	heuristic (name-prefix)	fail-open for the read-shaped set ONLY	Downgrades a low-risk read-shaped default-deny to Allow (decide.go:378); writes and self-modify still fail closed. The relaxation is name-based and conservative; Meta cannot widen authority.
require-witness (3)	structural (corroborates a git-checkable claim)	fail-closed (UNWITNESSED)	No claim, or a refuted claim, is held closed (kernel.go:223-230); the corroboration evidence is not agent-authored.
content / injection screen (MMU)	heuristic (regex + substring floor)	fail-closed on a hit, but evadable	The bare floor is “defeated by char-spacing, base64, homoglyph, zero-width, or bidi obfuscation” (recall.go:398-412). The structural property is the cross-process seal (clearance AND content re-screen AND witness, all independent), not detector completeness.
CI / git-evidence / keep-bit (4–6)	structural	fail-closed	The keep-bit is a non-forgeable AND of measured signals (shipgate.go:66-72); a candidate cannot pre-seed it (proofs_witness_test.go:27-29).

The rule the whole ladder turns on: a heuristic rung is allowed to be cheap and first, but it is never allowed to be the last word on a write or a self-modify. It either proves a refusal (deny) or it abstains and the structural rung above it decides. An INDETERMINATE result from a heuristic rung is the trigger to climb, not an excuse to wave through.

What already shipped vs what these epics add

The trust floor itself is done — epic #492 (“Wire the trust floor — close the Decide-vs-Syscall gap”) is CLOSED. That epic gave us the cost-ordered chain, the lattice fold, the per-call short-circuit, the require-witness gate, the deny-as-value disposition, and the non-forgeable keep-bit. None of the epics here reinvent that.

The model-routing spine is in flight — epic #595 with children #596–#605. #596 wires a single-model route, #598 does per-tool-call routing, #603 is routing observability (per-aspect decisions in /metrics). The residency gate already enforces ScopeTenant on the call side (internal/engine/engine.go:251-268). So the epics here do not touch routing-decision telemetry (that is #603) or the residency call gate — they add the orthogonal pieces: the result-side share-scope ceiling that is documented but unenforced (types.go:61 says “never shared more widely than its scope,” yet the only realization is clamping a tainted result down to ScopeAgent at internal/ifc/ifc.go:498 — the upward bound is never checked), and the rung-decision telemetry that is about which adjudication rung decided, a different surface from which model answered.

The RSI loop is done and gated — internal/rsiloop derives every witness (rsiloop.go:184-265), the keep-bit is non-forgeable, and the OBSERVE-only dos improve receipt seam (#588) is wired without re-gating. The epics here do not re-gate the keep-bit through dos improve (that erodes non-forgeability and is a known live trap); the least-rung shipgate epic stays on the measurement side.

What is genuinely unbuilt is the lazy-escalation half of the doctrine: the chain-level short-circuit, the INDETERMINATE verdict, per-claim risk-to-rung selection, the complain->shadow->enforce promotion ledger, granular integrity rung selection, the smallest-sufficient-evidence subset in the shipgate, the per-task capability bounding set, and the CLI/telemetry surface that reports which rung decided each claim. Those are the epics in the companion roadmap, verification-ladder-epics.md.

Closing posture

fak’s adjudicator is already a most-restrictive-wins, cost-ordered, fail-closed reference monitor — structurally the same machine as seccomp’s filter fold and the LSM stack. The work ahead is not to make it stricter; it is to make it lazier in the good sense: stop at the cheapest rung that conclusively decides, give the cheap rungs a way to say “I could not decide, climb,” and let an operator see and tune which rung carried each claim. Restrictiveness is solved. Flexibility — granular, smallest-sufficient, observable — is the next epic line.

The gaps these epics close

The lazy-escalation half of the doctrine, enumerated against HEAD:

1. Chain-level fold never short-circuits: kernel.go:185-194 evaluates EVERY adjudicator even after a rank-100 Deny is already maximal, so the deny path is always O(full-chain) instead of O(first-conclusive-rung). The per-call short-circuit exists (decide.go:255-374) but the chain-level one does not.
2. No INDETERMINATE verdict. The only abstention is VerdictDefer (‘I have no opinion’), which folds to DEFAULT_DENY when nothing allows (kernel.go:195-197). There is no verdict that means ‘I could not CONCLUSIVELY decide this cheaply — a costlier rung MUST be consulted before commit’, distinct from both fail-open and fail-closed. A cheap heuristic rung therefore cannot signal ‘climb’ without either falsely denying or falsely abstaining.
3. No per-claim risk-based rung selection. The per-call rung ORDER and which rungs run is hard-coded in decide.go:255-374 (only LintWrites is opt-in). You cannot say ‘a low-risk read needs only the name rung’ vs ‘a write into a shared tree needs arg-predicate + lint’; every call that reaches a rung pays it, and the rungs are not data-driven or reorderable.
4. shipgate is all-three-or-revert with no smallest-sufficient subset. improvedBit = improved() && SuiteGreen && TruthClean is a flat AND (shipgate.go:67); there is no path that establishes the keep property from a cheaper sufficient subset (e.g. a docs-only change skipping the suite, or a proof-carrying change skipping re-measure). Every candidate pays the full ms-spawn worktree + suite (shipgate.go:110-130).
5. No observe -> shadow -> enforce promotion path. AdmitAndLog is a single GLOBAL per-policy binary that only relaxes a hard-coded read-prefix set (decide.go:377-389, 224-235). There is no per-tool complain dial and no PROMOTION LEDGER that counts ‘tool X logged N clean would_deny events with zero benign regressions, therefore promote X to enforce’ — the AppArmor complain->enforce step is a manual operator decision, not an accumulated, witnessed counter.
6. Result-side admit fold is narrower than the call-side ladder. admitResult acts only on Quarantine and Transform; a result-side Deny or RequireWitness silently falls through to ‘admitted’ (kernel.go:280-282). A bad RESULT cannot be hard-refused or sent to handback — the result ladder is missing the top rungs the call ladder has.
7. Result-side ShareScope ceiling declared but unenforced. types.go:61 states ‘a result is never shared more widely than its scope’, but the only realization is clamping a TAINTED result DOWN to ScopeAgent at ifc/ifc.go:498. Nothing checks the UPWARD bound on the share path — a result tagged ScopeFleet/ScopeTenant is not provably confined to that boundary when shared. (Note: the residency CALL gate at engine/engine.go:251-268 DOES enforce ScopeTenant -> no-remote-route; the gap is the result-side share ceiling, not the call-side route.)
8. Rate limiting is env-only. internal/ratelimit is wired (registrations.go:53) and enforces a RATE_LIMITED -> WAIT cap, but it is configured ONLY by FAK_RATELIMIT_* env vars read once at process start; the policy-manifest ‘rate_limit:’ field is deliberately deferred (ratelimit.go:31-34). An operator cannot express a per-tool/per-tenant rate cap declaratively, and WAIT carries no retry-after duration (Disposition returns a bare token, kernel.go:478-489).
9. No per-task capability bounding set or monotone-shrink latch. Policy is a flat global object; there is no delegate-minus where a spawned sub-step/synth-tool inherits a SUBSET of the caller’s grants it can only shrink, and no no_new_privs-style sticky latch that forbids re-widening the allow-set for the rest of a trajectory. fak can DEFAULT_DENY but cannot automatically compute and drop to the least rung/least authority that still passes.
10. Which rung decided is computable but not surfaced. FoldExplain already produces a per-rung Decision trace with a Winner bool (kernel/explain.go:74), but it is ‘built only off the hot path’ and exposed through no CLI or /metrics counter. Flexibility is therefore not OBSERVABLE — an operator cannot see the rung-decision distribution to know which rungs are load-bearing or tune the ladder the way dos enforce-tune tunes policy knobs.
11. Registered escalation kinds are rank-indistinguishable and route identically. FoldRank forces every unknown registered kind to 100 (registry.go:859), so two distinct escalation kinds order nondeterministically relative to each other, and Submit collapses every kind above the core into ONE fail-closed deny branch (kernel.go:352-363). ‘Page a human’ vs ‘defer to a peer’ vs ‘hard-kill the call’ cannot be routed differently without a core edit.
12. vDSO hit is a blanket Allow that bypasses the whole ladder. A FastPath hit (kernel.go:303-314) returns Allow with no adjudication and no result-side gate; correctness rests entirely on Lookup only hitting provably-safe calls. There is no cheap per-tier re-check between a vDSO hit and Allow, so a poisoned cache entry skips the lattice entirely — the one rung that is fail-open by construction.

The epic line

Eight epics build the missing half. The keystone is Epic 1 (it adds the verdict and the lazy fold the others lean on); Epics 2 and 4 build on the fold semantics. Full drafts — problem, file:symbol current state, graduated rungs, acceptance, child issues, honesty boundary — are in verification-ladder-epics.md. They are tracked on GitHub under roadmap issue #705, each epic carrying its own child issues.

#	Epic	Tracked
1	feat(kernel): VerdictIndeterminate + lazy chain fold — short-circuit on the first conclusive rung, escalate only on a residual abstain	#657
2	feat(adjudicator): per-claim risk-class RungProfile — restrict-only, data-driven rung selection (default the smallest sufficient rung)	#663
3	feat(adjudicator): per-tool complain → shadow → enforce promotion ledger (AppArmor/eBPF analogue)	#669
4	feat(kernel): result-side ladder parity — honor Deny/RequireWitness on admitResult	#674
5	feat(shipgate): smallest-sufficient-evidence keep-bit (graduated EvidenceProfile, default all-three)	#680
6	feat(engine): result-side ShareScope ceiling enforcement — confine a result to its declared scope on the share/readmit path	#687
7	feat(observability): rung-decision telemetry — make the adjudication ladder OBSERVABLE (a labeled /metrics counter over the verdict stream)	#693
8	feat(adjudicator): policy-manifest rate_limit + retry-after on WAIT (declarative throttle rung)	#699