Non-Verbal Proof: AST Invariants, Green Traces, and Exit Code 1#

An LLM will tell you the code is correct. It will do so fluently, with citations to files it did not read, with a recitation of tests it did not run, and with a closing sentence that sounds like a senior engineer signing a change. That sentence is not a proof. It is a sample from a next-token distribution.

Nomos treats that sample as zero-value signal.

Non-Verbal Proof is the substrate law that replaces conversational assurance with compiled predicates. The engine does not ask the model whether a mutation is sound. It parses the mutation into an abstract syntax tree, measures structural invariants against hard ceilings, executes a hermetic test harness, and inspects a process exit status. The only language the state machine accepts at a phase boundary is:

exit 0  →  transition
exit 1  →  refuse

Everything else — prose, confidence, “I have fixed the issue,” a green checkmark emoji in a chat log — is discarded before it reaches the transition table.

This chapter specifies that law as a machine, not as a slogan.

1. Why Verbal Proof Is Not Proof#

The 2024–2026 failure mode called vibe coding had a characteristic signature: the model authored implementation and tests in the same pass, then reported success. Two defects followed with high probability.

Tautological tests. The implementation contained a logic inversion. The test asserted the inverted logic. The suite was green. The feature was wrong. The model, asked whether the work was correct, answered yes — because the tokens “the tests pass” were locally consistent with the tokens it had just emitted.

Hallucinated agreements. A REVIEW prompt asked “does this satisfy the spec?” The model produced a narrative alignment: every bullet in the spec mapped to a function name that existed, or to a function name that sounded like it existed. No AST walk occurred. No import graph was closed. No failing test was ever observed. The conversation recorded consensus. The binary recorded nothing.

Verbal proof fails for a structural reason, not a moral one. A language model is a bounded heuristic subroutine — a stochastic ALU. It can propose mutations. It cannot certify them, because certification is not a linguistic act. Certification is a measurement of a program against a predicate that does not care what the program was intended to mean.

Axiom 3 of the substrate (Non-Verbal Proof) and Axiom 6 (Epistemic Distrust) are the same fact stated twice:

Generating code is low-cost probabilistic token streaming. Proving code is structural and mathematical. Self-reported success is treated as zero-value signal. Verification requires exit code 0 from compiled binaries.

The dual-core split follows immediately. The Intent core (the model) explores. The Substrate core (compiled Go) verifies. Those two cores must never occupy the same layer. If they do, the verifier can be talked out of verifying.

2. The Predicate, Not the Prompt#

A phase transition in Nomos is a function of machine state, not of dialogue:

Verify : Worktree × GateSet → {0, 1}

GateSet is a compiled collection of Definition of Done (DoD) predicates. Each predicate is a Go function that walks an AST, a test trace, or a package graph and returns a boolean. The aggregator is conjunctive and total: one false gate yields process exit 1. There is no weighted score, no “mostly green,” no advisory channel the agent can interpret as optional.

type Gate struct {
    Name string
    Run  func(ctx context.Context, wt Worktree) error
}

func Verify(ctx context.Context, wt Worktree, gates []Gate) int {
    for _, g := range gates {
        if err := g.Run(ctx, wt); err != nil {
            // Structured JSON diagnostic. Never prose.
            report.Fatal(g.Name, err)
            return 1
        }
    }
    return 0
}

Two properties of this function are load-bearing.

Silence of success. A passing gate emits no narrative. Advisory diagnostics are forbidden (Axiom 12, Binary Diagnostics). Agents treat warnings as ambiguous: they either ignore structural debt or burn the step budget “fixing” harmless notices. The substrate therefore has two states only: PASS and FATAL.

Uninterpretability of failure. Exit code 1 is not a suggestion. It is not a lint the model may acknowledge and proceed past. The lifecycle state machine (TRIAGE → SPEC → PLAN → EDIT → REVIEW → SYNC → LEARN) will not fire the next transition. Capability tokens for the subsequent phase are not issued. The worktree remains dirty, isolated, and unmergeable.

The agent cannot negotiate with os.Exit.

3. What the AST Is Allowed to Be#

Static analysis in Nomos is not a style guide. It is a set of physical bounds on the shape of code an untrusted generator is permitted to leave in a worktree. The analyzer is go/ast + go/types + package-graph closure, compiled into nomos verify. It does not call the model. It does not ask for intent. It measures.

3.1 Cyclomatic complexity ceiling: (M < 15)#

McCabe complexity (M = E - N + 2P) is computed per function from the control-flow graph recovered from the AST. The ceiling is 15. Not 15 “unless the function is important.” Not 15 “with a waiver comment.” Fifteen.

The bound is not aesthetic. It is a truncation hedge. Functions above this ceiling concentrate branching that a context window will summarize, stub, or invert on the next edit. Under window pressure, models delete else arms, collapse error paths into _ = err, and leave the happy path looking complete. A complexity ceiling forces the slice before the model is tempted to truncate (Axiom 4, Topological Slicing; Axiom 8, Non-Destructive Refactoring).

func complexity(fn *ast.FuncDecl) int {
    n := 1
    ast.Inspect(fn, func(n0 ast.Node) bool {
        switch n0.(type) {
        case *ast.IfStmt, *ast.ForStmt, *ast.RangeStmt,
            *ast.CaseClause, *ast.CommClause:
            n++
        case *ast.BinaryExpr:
            // && and || are additional decision points
        }
        return true
    })
    return n
}

A function that measures 15 or above fails the gate. The prescribed repair is extraction into sibling functions under the same package, with AST symbol parity preserved. Commenting out branches to “reduce complexity” is itself a gate failure: the analyzer compares exported signatures and statement density against the pre-edit AST. Destructive omission is not modularization.

3.2 Docstring density: (\rho ≥ 0.10)#

Let (C) be the count of documentation comments attached to exported declarations, and (E) the count of exported declarations. The gate requires (\rho = C/E ≥ 0.10) at package scope, and a stricter local check: every exported func, type, var, and const must carry a doc comment that is not a copy of the identifier.

This is not a civility rule. Documentation comments are the only durable interface between a mutation and the next agent that must read it without the original prompt. Models under pressure emit // TODO and // helper and paste the same sentence onto five functions. The analyzer rejects:

• missing docs on exported symbols
• docs whose normalized token set is a subset of the identifier
• boilerplate cloned across sibling declarations (near-duplicate comment hashing)

Axiom 8 again: comment density is part of AST preservation. A refactor that splits a file and drops docs has destroyed information even if types still compile.

3.3 Hermetic import graphs#

A package’s import set must be closed under the plane and layer it claims to inhabit. The analyzer builds the import DAG from go/packages and applies three closures:

1. Plane closure. Substrate packages (nomos-substrate) must not import Membrane or Intent runtime types. Intent is data (Markdown, schemas) consumed as bytes, not as a Go module of policy. Membrane is a projection; it is never a dependency of a gate.
2. Layer closure. Domain packages do not import CLI, SQLite driver internals, or worktree scaffolding. Inversion of control stays in the engine. Libraries do not grow a main.
3. Stdlib-and-allowlist closure. Third-party imports are an explicit allowlist in the package manifest. An undeclared module path is a hard fail. “It compiled on my laptop” is not a closure.

Hermeticity here is cognitive as well as build-theoretic. An unconstrained import is an unconstrained context surface. The next model invocation will read through that import, saturate the window, and begin inventing APIs that exist two modules away.

3.4 Circular dependency ban#

The import DAG must be acyclic. This is the Go compiler’s rule, restated as a DoD gate so that the failure is named in the same JSON diagnostic schema as complexity and tests. Cycles are not “a packaging inconvenience.” They are a phase-leakage hazard: two packages that import each other cannot be reasoned about, tested, or sliced independently, which is exactly how a swarm of Tier-2 workers ends up editing the same cycle from two worktrees.

The gate emits the cycle as an ordered list of import paths. The repair is unidirectional extraction of a third package that both depend on, or inversion of the dependency. There is no var _ = import hack that satisfies the gate; blank imports used for side effects are themselves a named failure class unless they appear on an explicit register (e.g. database drivers listed in the manifest).

3.5 What the AST must still be#

Compilation and go vet are gates, not assumptions. Zero syntax errors, zero type errors, zero vet findings. Constructive type proof precedes runtime proof: if the program is not a well-typed Go program, the test harness is not run. We do not spend the sandbox on an ill-typed tree.

Dead code, severed wires, and zombie exports are AST-reachable facts. An exported function with no intra-module reference and no test reference is a fail. An HTTP route registered in a table that no handler implements is a fail. These are not “cleanup nits.” They are the residue of a model that stubbed its way to a green compile.

4. Green Traces, and Why Green Is Not Enough by Itself#

A green trace is the structured record of a test run in which every case passed, no test was skipped without a gate-level exemption (Nomos has none), and the process exit status was 0. The trace is JSON. It names packages, cases, elapsed time, and the binary hash of the test executable. Conversational summaries (“all tests passed”) are not traces.

100% green is necessary and insufficient.

Necessary: a red suite cannot leave EDIT, cannot enter REVIEW as passing, and cannot be 2PC-merged to a plane trunk. The state machine does not have a path for “ship with known failures.”

Insufficient: tautological tests are green. Tests authored after the implementation, fitted to its accidents, are green. Tests that re-assert the implementation’s inverted boolean are green.

Hence the TDD solver loop is not a methodology preference. It is a temporal invariant on the trace: the suite must have been observed red on the new predicates before it is observed green on those same predicates.

5. The TDD Solver Loop#

Cognitive inversion says the compiled runtime drives the lifecycle, and the model is called with ephemeral CapBAC budgets. TDD is that inversion applied to the inner loop of a single task.

PLAN  →  TEST_FIRST  →  EDIT  →  REVIEW  →  SYNC
              │              │         │
              │              │         └─ 39 DoD gates, including AST + green trace
              │              └─ minimal mutation until the same predicates pass
              └─ predicates exist, execute, and fail for the stated reason

5.1 PLAN#

The agent inspects interfaces and writes implementation_plan.md: behavior, package boundaries, and the names of the predicates that will witness success. No application source is mutated. The plan is data in the Intent plane. The substrate does not execute it; it records that a plan exists and that a human (or Tier-1 orchestrator) signed it. Unsigned plans do not issue a TEST_FIRST capability.

5.2 TEST_FIRST#

Before any production .go file in the task’s blast radius is edited, the agent authors unit tests that assert the new behavior. nomos verify --phase=TEST_FIRST then requires all three:

1. The test package compiles.
2. The new tests run.
3. The new tests fail, and the failure matches a declared invariant (wrong result, missing symbol, failing equality) — not a compile error in the test itself, not a skipped test, not a timeout that might be infrastructure.

If the new tests pass against current HEAD, the gate fails. The agent has asserted a behavior the system already has, or has written a vacuous test. Either way, there is no work.

This is Axiom 14 (Bidirectional Verifiability) as a phase lock: an agent cannot enter EDIT without a deterministic gate that fails on current state and will pass only upon correct completion.

5.3 EDIT#

The MutationCapability is issued only in EDIT, is non-transferable, and expires at the phase boundary. The agent writes the minimal implementation that satisfies the failing tests. “Minimal” is enforced negatively: diffs that touch files outside the plan’s blast radius fail a path-allowlist gate; diffs that delete or stub existing exported symbols fail AST parity.

When the agent believes it is done, it does not say so. It returns control. The engine re-runs the harness.

5.4 REVIEW#

nomos verify executes the full DoD set — compilation, typechecking, cyclomatic ceilings, docstring density, import closure, cycle ban, goroutine leak checks, secret hygiene, phase-token validity, and the now-green trace with test-first parity.

Test-first parity is a mechanical diff of traces:

trace_red  = TEST_FIRST run (must contain failing cases F)
trace_green = REVIEW run  (must contain the same case IDs, all passing)
parity     = IDs(F) ⊆ IDs(REVIEW)  ∧  failures(REVIEW) = ∅

If the green suite no longer contains the cases that were red, the agent deleted or renamed the tests to obtain a green run. That is a fail. The tests are part of the proof object, not a disposable scaffold.

5.5 The solver, not the author#

On gate failure the engine does not open a chat. It emits structured JSON, decrements the step budget, and — if budget remains — re-enters EDIT with the diagnostic as the sole new context. This is a damped control loop, not a debate. Recursion is finite. Exhaustion of budget with remaining FATAL gates leaves the worktree unmerged and tears it down. Trunk is untouched.

The model is a solver against a frozen predicate. It is not a co-author of the predicate. If the predicate is wrong, a human amends the plan and the TEST_FIRST artifacts; the model does not get a vote on lowering the cyclomatic ceiling.

6. Exit Code 1 as an Un-Negotiable Machine Constraint#

Unix process status is the narrowest, oldest, least rhetorical interface we have. Nomos uses it because it cannot be paraphrased.

nomos verify
echo $?    # 0 or 1. Nothing else is defined.

The lifecycle state machine is a compiled table. A sketch of the REVIEW→SYNC edge:

type Phase int

const (
    PhaseEdit Phase = iota
    PhaseReview
    PhaseSync
)

func (sm *Machine) Step(ctx context.Context) error {
    switch sm.phase {
    case PhaseReview:
        code := Verify(ctx, sm.worktree, DoDGates)
        if code != 0 {
            sm.record(EventVerifyFail)
            return ErrBlocked{Code: 1, Phase: sm.phase}
        }
        return sm.transition(PhaseSync) // issues SyncCapability
    case PhaseSync:
        return sm.twoPhaseCommit(ctx)
    }
    return nil
}

Properties that must remain true:

No override flag. There is no --force, no --no-verify, no environment variable that the model can set inside the sandbox to skip gates. Axiom 5 (Canonical Singularity): a skip flag is a second representation of “verified,” and second representations are how agents escape predicates. Pre-commit hooks on plane trunks independently refuse commits whose tree was not produced by a passing nomos verify in a registered worktree.

No partial merge. 2PC release requires the verify receipt (Ed25519-signed, attached to refs/notes/agent) as a precondition of the merge commit into the plane trunk (substrate, intent, membrane, infra). A missing receipt is indistinguishable from exit 1.

No conversational escalation. The model cannot open a higher-privilege tool to “approve anyway.” CapBAC tokens are phase-scoped. REVIEW has VerifyCapability. It does not have MergeCapability. The orchestrator cannot hand the worker a merge token; the engine never mints one unless Verify returned 0.

Binary diagnostics only. The payload on exit 1 is JSON:

{
  "gate": "ast.complexity",
  "pkg": "internal/worktree",
  "func": "reconcileLocked",
  "metric": 18,
  "ceiling": 15,
  "exit": 1
}

The worker’s next EDIT prompt is this object, not a paragraph about code quality. Ambiguous prose is how models spend budget on the wrong repair.

Exit code 1 is therefore not a developer experience choice. It is the object-capability boundary of the system. If a path exists from “the model would like to proceed” to “trunk mutated” that does not pass through exit 0, the system is no longer Nomos. It is a chatbot with a git remote.

7. The 39 Gates, Compressed to What This Chapter Owns#

The full DoD set spans eight dimensions. This chapter owns the proof-theoretic core. The others exist so that a green, simple, well-documented, acyclic package still cannot smuggle a secret, a leaked goroutine, or a phase-token forgery onto trunk.

REVIEW is not a model “looking over the diff.” REVIEW is this table, executed in a subshell, against a hash-pinned worktree.

8. What the Agent Is, Under This Law#

Under Non-Verbal Proof the agent is not a colleague you trust and then audit. It is a Byzantine proposer in a state machine that does not take testimony.

The proposer may emit any diff the MutationCapability allows. The verifier, which does not share memory with the proposer, measures the tree. If the measurement is 0, the 2PC engine may merge and tear down the worktree. If the measurement is 1, the proposer is invoked again with less budget, or the task dies. Trunk never hears about it.

This is why the substrate is compiled Go and not a prompt chain. A prompt chain can be argued with. An AST walk cannot. A test binary cannot. os.Exit(1) cannot.

The engineering consequence is unromantic and sufficient: we stop asking models if they are finished. We finish when the predicates say 0.

Substrate  ──invokes──►  stochastic ALU  ──mutates──►  worktree
    ▲                                                    │
    └──────────── Verify() → {0,1} ◄─────────────────────┘
                 (AST · imports · density · trace)

That loop is the entire epistemology of the inner cycle. The rest of the handbook is topology, isolation, and how proofs are projected outward without being rewritten as opinions.