---
title: "The Verification Ladder: flexible, granular, smallest-sufficient-rung adjudication"
description: "fak's doctrine for graduated verification — default to the cheapest rung that can conclusively decide a property, escalate only on an INDETERMINATE verdict or warranted risk. The agent-kernel analogue of seccomp's restrictiveness fold, least-privilege capability sets, AppArmor complain->enforce, the integrity granularity ladder, and the eBPF prove-before-admit verifier."
---

# 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](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 `Defer`s (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](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](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 |
