Paper deep dive

Nidus: Externalized Reasoning for AI-Assisted Engineering

Danil Gorinevski

Year: 2026Venue: arXiv preprintArea: cs.SEType: PreprintEmbeddings: 53

Intelligence

Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 93%

Last extracted: 4/10/2026, 3:00:58 AM

Summary

Nidus is a governance runtime for AI-assisted software engineering that mechanizes the V-model by using a 'living artifact'—a single S-expression-based object that unifies requirements, architecture, design, and proof obligations. It ensures engineering invariants through a decidable verification kernel that validates every mutation before persistence, preventing governance theater and ensuring monotonic growth of the obligation set.

Entities (6)

Nidus · software-system · 100%Z3 · smt-solver · 100%V-model · engineering-methodology · 95%Claude · llm · 90%Codex · llm · 90%Gemini · llm · 90%

Relation Signals (3)

Nidus → mechanizes → V-model

confidence 95% · We present Nidus, a governance runtime that mechanizes the V-model for AI-assisted software delivery.

Nidus → uses → Z3

confidence 95% · Z3 validates constraint composition at guidebook authoring time.

Claude → delivered → 100,000-line system

confidence 90% · three LLM families (Claude, Gemini, Codex) delivered a 100,000-line system

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:We present Nidus, a governance runtime that mechanizes the V-model for AI-assisted software delivery. In the self-hosting deployment, three LLM families (Claude, Gemini, Codex) delivered a 100,000-line system under proof obligations verified against the current obligation set on every commit. The system governed its own construction. Engineering invariants - traced requirements, justified architecture, evidenced deliveries - cannot be reliably maintained as learned behavior; assurance requires enforcement by a mechanism external to the proposer. Nidus externalizes the engineering methodology into a decidable artifact verified on every mutation before persistence. Organizational standards compile into guidebooks - constraint libraries imported by governed projects and enforced by decidable evaluation. Four contributions: (1) recursive self-governance - the constraint surface constrains mutations to itself; (2) stigmergic coordination - friction from the surface routes agents without central control; (3) proximal spec reinforcement - the living artifact externalizes the engineering context that RL and long-chain reasoning try to internalize; the specification is the reward function, UNSAT verdicts shape behavior at inference time, no weight updates; (4) governance theater prevention - compliance evidence cannot be fabricated within the modeled mutation path. The constraint surface compounds: each obligation permanently eliminates a class of unengineered output. The artifact's development history is a formal development - every state satisfies all active obligations, and the obligation set grows monotonically.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

53,059 characters extracted from source content.

Expand or collapse full text

Nidus: Externalized Reasoning for AI-Assisted Engineering Danil Gorinevski * research@cybiont.com April 5, 2026 Abstract We present Nidus, a governance runtime that mechanizes the V-model for AI-assisted software delivery. In the self-hosting deployment, three LLM families (Claude, Gemini, Codex) delivered a 100,000-line system under proof obligations verified against the current obligation set on every commit. The system governed its own construction. Engineering invariants—traced requirements, justified architecture, evidenced deliveries— cannot be reliably maintained as learned behavior; assurance requires enforcement by a mecha- nism external to the proposer. Nidus externalizes the engineering methodology into a decidable artifact verified on every mutation before persistence. Organizational standards compile into guidebooks—constraint libraries imported by governed projects and enforced by decidable evalu- ation. Four contributions: (1) recursive self-governance—the constraint surface constrains mutations to itself; (2) stigmergic coordination—friction from the surface routes agents without central control; (3) proximal spec reinforcement—the living artifact externalizes the engineering context that RL and long-chain reasoning try to internalize; the specification is the reward function, UNSAT verdicts shape behavior at inference time, no weight updates; (4) governance theater prevention—compliance evidence cannot be fabricated within the modeled mutation path. The constraint surface compounds: each obligation permanently eliminates a class of unengineered output. The artifact’s development history is a formal development—every state satisfies all active obligations, and the obligation set grows monotonically. 1 Introduction Engineering is not code. Engineering is the chain of invariants that makes code trustworthy: every requirement traced, every architecture decision justified, every delivery evidenced. The V-model— requirements→architecture→design→verification→evidence—encodes these invariants. It remains the standard in safety-critical domains (ISO 26262, DO-178C, IEC 62304). LLM agents produce code with more defects [16] and no traceability. The problem is not capability. RLVR [14] and process reward models show that training can improve adherence to external verifiers—but the verifier remains the source of assurance, not the trained policy. Engineering invariants cannot be reliably maintained as learned behavior; they must be enforced by a mechanism external to the proposer. Training data captures what engineers did; it does not capture the rules they maintained. A model that “knows” traceability from textbooks will approximate it, * cybiont GmbH, Kantonsstrasse 17, 8862 Schübelbach, Switzerland. ORCID: 0009-0007-5992-6667 1 arXiv:2604.05080v1 [cs.SE] 6 Apr 2026 and the approximation degrades under pressure—an agent fabricates evidence (Section 7), another skips synthesis gates because “I optimize for speed over correctness.” You do not train a compiler to reject type errors; you build a type checker. Test-driven development (TDD) bridges code correctness. Planning layers attempt to bridge the rest: agent frameworks generate implementation plans, add stateful workflows, add persistent state. These are useful—but in each case the model proposes the plan and the model verifies the plan. For safety-critical invariants, self-assessment is not sufficient; an external, decidable mechanism is required. Nidus externalizes the methodology into a decidable artifact. Requirements, architecture, design, traces, proofs, and evidence live in a single object—a living artifact—verified on every mutation before persistence. Organizational standards compile into guidebooks—constraint libraries any project imports. The methodology is in the environment, enforced by decidable evaluation; Z3 validates constraint composition at guidebook authoring time. The architect provides what models cannot: judgment about what to build and how to structure it. Requirements, architecture decisions, design elements, and the development vector are human input. Three LLM families (Claude, Gemini, Codex) delivered the reference implementation through this governance loop. The reference implementation uses S-expressions because they are SMT-LIB2 [4]: a solver- aligned representation that minimizes translation between the artifact and the solver [2]. The tools for decidable verification—S-expressions [1], SMT solvers, decidable logics—have existed for decades. What changed is the rate of the proposer. We call the union of proof obligations, guidebook constraints, and monotonic invariants the constraint surface (formally defined in Section 3). Four contributions: (1) recursive self-governance— the surface constrains mutations to itself (Section 4); (2) stigmergic coordination—friction from the surface routes agents without an orchestrator (Section 5); (3) proximal spec reinforcement—the artifact externalizes what RL and planning layers try to internalize (Section 6); (4) enforcement mechanisms—governance theater prevention, SOP gate sequences, lesson provenance (Section 7). 2 Nidus: A Decidable Living Specification What does the living artifact look like in practice? Nidus replaces codebases with a living spec- ification: the S-expression is the design, the proof obligation set, and the governance authority. Implementation code, RTL, and documentation are governed through anchor paths (code-paths, test-paths) and proof obligations. 2.1 Representational Closure The living artifact serves four roles simultaneously: the database (for the daemon that enforces mutations), the solver input (for Z3 that checks proof obligations), the agent context (an LLM ingests the entire artifact in one read), and the specification (a human reads the same object the solver checks). We call this representational closure [1]: every participant—human, LLM, solver—reads, writes, and reasons over the identical object. In traditional engineering, this state is fragmented: requirements in Jira, architecture in Conflu- ence, traces in spreadsheets, test results in CI logs. The living artifact unifies them—primarily for the AI agents, which need the full engineering state in their context window. An agent that cannot see the traces cannot maintain them; an agent that cannot see the proof obligations cannot satisfy 2 them. The invariant chain becomes a structural property of the object, not a behavioral property of whoever writes to it. 2.2 Annotated Example Circled numbers1–12mark every structural element; Section 2.3 maps each to a mathematical object. Listing 1: Annotated Nidus artifact. (nidus-system "Interceptor"1 (requirements2 (req UR-01 (kind sovereignty) (source RAD) (shall "All classification executes locally") (constraint (never (payload-egress data)))) (req FR-01 (kind functional) (source D) (shall "Verdict is one of ALLOW BLOCK WARN"))) (architecture3 (component Interceptor (responsibility "Intercept and route traffic")) (component Brain (responsibility "Local classification")) (connector Interceptor Brain 4 (flow CLASSIFY) (protocol synchronous))) (design 5 (value-object Verdict (values ALLOW BLOCK WARN))) (workflows6 (workflow classify-flow (states idle classifying decided) (initial idle) (transition idle classifying (guard (> priority 0))) (transition classifying decided (guard (< elapsed 100))))) (features 7 (feature FEAT-01 (name "Local classification engine") (status claimed) (scope (requirements UR-01 FR-01) (code-paths "src/brain.py")))) (traceability8 (trace TR-01 UR-01 Brain Verdict) (trace TR-02 FR-01 Brain Verdict)) (proof-obligations9 (proof PO-TRACE-01 (kind traceability-complete) (description "Every requirement has a trace")) (proof PO-CONN-01 (kind connector-integrity) (description "Connectors reference components")) (proof PO-DAG-01 (kind dag-enforcement) (description "No dependency cycles")) 3 (proof PO-WF-01 (kind workflow-satisfiability) (description "Workflow guards are satisfiable"))) (coordination 10 (claim (agent opus-a1b2) (feature FEAT-01) (lease-expires "2026-03-20T14:00:00Z"))) (guidebooks 11 (imports "../epoch.guidebook.epoch"))) ;; Sidecar file: .epoch.friction.epoch12 (agent-friction-ledger (events (friction-event FX-01 (kind agent_rejection) (agent gemini-8536) (timestamp "2026-03-09T21:42:03Z")))) A connector 4 is a typed data-flow edge. A workflow 6 is an FSM with QF_LIA guards. Features 7carry scope: which requirements, code-paths, and test-paths belong to the delivery. A trace8 links requirement→component→design element. Proof obligations9are predicates over the artifact’s finite sections, evaluated on every mutation. Each has akindthat names a verification cate- gory—traceability-complete,connector-integrity, etc.—and binds to an evaluator function in the kernel. Obligations span structural, schema, SMT, temporal, and domain-specific kinds. Two layers of DAG enforcement illustrate the distinction: the localPO-DAG-01(kinddag-enforcement) checks that components form an acyclic dependency graph, while the inheritedGC-MODULE-DAG (kindcall-graph-dag) checks that Lisp modules in the daemon codebase have no circular imports. Both are DAG checks, but over different sections of the artifact. Example. An agent adds requirementFR-02without a corresponding trace.PO-TRACE-01 (traceability-complete) rejects: FR-02 has no trace link. The agent adds(trace TR-03 FR-02 Brain Verdict). All POs pass; persisted. The loop: propose, verify, repair, commit. Coordination10: claims with leases. Friction ledger12: append-only sidecar for agent-quality signals. Guidebook imports 11 . The Interceptor project defines four local proof obligations (PO-TRACE- 01 through PO-WF-01). But line11imports an organizational guidebook. That guidebook carries additional constraints—engineering standards the project inherits without defining them locally: Listing 2: Guidebook constraints inherited via (imports ...) in Listing 1. ;; From epoch.guidebook.epoch (imported by Interceptor) (guidebook-constraint GC-SCOPE-COMPLETENESSA (z3_formula (implies feature_deliveredB (and has_code_paths has_test_paths has_requirements))) (po-kind feature-code-test-symmetry)C (description "Delivered features must have code-paths, test-paths, and requirements")) (guidebook-constraint GC-MODULE-DAGA (z3_formula (and (not parse_imports_query)B (not mutate_imports_query) (not verify_imports_query))) (po-kind call-graph-dag)C (description "Module DAG: no back-edges")) 4 (guidebook-constraint GC-EVIDENCE-PROVENANCEA (z3_formula (implies evidence_submitted B (and witness_registered hash_present))) (po-kind evidence-provenance) C (description "Evidence requires registered witness and server-computed hash")) AConstraint identity.BSMT formula: compiled to native Z3 Boolean assertions (Section 3 details the compilation).CPO-kind binding: links to an evaluator function that iterates artifact sections and returns violations. Terminology note:kindvs.po-kind. Inside the artifact (Listing 1), a proof obligation’skind names the verification category it belongs to—e.g.traceability-complete. Inside a guidebook constraint (Listing 2), thepo-kindfield serves the same purpose: it identifies the evaluator function the kernel dispatches. The two are the same namespace; the separate keyword exists because a guidebook constraint also carries a z3_formula, whereas a local PO relies solely on its evaluator. Each constraint has two enforcement paths. Thepo-kindevaluator traverses the artifact’s finite sections and returns violations or nil. Thez3_formulacompiles to a Z3 assertion checked for satisfiability. Many constraints use both: the evaluator performs the structural check; the formula provides a declarative specification the solver verifies independently. Why guidebooks matter. Without the import on line 11 , the Interceptor ’s four local POs would ac- cept a delivery withcode-pathsbut notest-paths—traceability is complete, connectors are valid, the DAG is acyclic, and the workflow guards are satisfiable. With the import, the organizational guidebook addsGC-SCOPE-COMPLETENESS, which requirestest-pathson every delivered feature. Agentopus-a1b2attempts to deliver FEAT-01 (Listing 1, currentlyclaimed). The mutation changes status todelivered. The daemon evaluates all obligations—local and inherited—against the proposed state: Listing 3: Verification output: local POs pass, inherited constraint rejects. commit_change_set: verify FEAT-01 delivery PO-TRACE-01 traceability-complete PASS PO-CONN-01 connector-integrity PASS PO-DAG-01 dag-enforcement PASS PO-WF-01 workflow-satisfiability PASS -- inherited from epoch.guidebook.epoch -- GC-MODULE-DAG call-graph-dag PASS GC-EVIDENCE-PROV. evidence-provenance PASS GC-SCOPE-COMPLETE. feature-code-test-sym. FAIL FEAT-01: has code-paths, missing test-paths z3: (implies feature_delivered (and has_code_paths has_test_paths has_requirements)) -> UNSAT REJECTED: 1 violation (GC-SCOPE-COMPLETENESS) The agent adds(test-paths "tests/test_brain.py")to the scope and retries; all obligations pass; FEAT-01 is delivered. The organizational standard was enforced mechanically—the Intercep- tor project never defined this constraint. Inheritance is monotonic (Definition 5):Π(G parent ) ⊆Π(G child ). Three layers compose: code practices (DAG, function length, naming), engineering process (scope completeness, TDD evidence, claim-before-work), and anti-theater (evidence provenance, claim-before-dispatch). Every governed project inherits all three—the methodology is a reusable proof library. 5 Guidebooks as domain introduction.Guidebooks carry more than constraints. A(modules ...) declaration names domain-specific Lisp modules that the daemon loads on demand when any project imports the guidebook. The chip-design guidebook declares four modules—an RTL parser, five hardware PO evaluators, a synthesis checker, and a simulation evidence gate—alongside eight constraints and onboarding templates. A single(imports "chip-design.guidebook.epoch") line gives the verilog project a complete hardware governance stack: constraint enforcement, domain-specific verification, and tool integration. The kernel does not change. Adding a new domain (VHDL, Chisel, a compliance framework) means writing a guidebook and its modules— not modifying the daemon. Each module must export a set of named evaluator functions; every evaluator accepts the artifact’s parsed S-expression tree plus the mutated section, and returns either nil(pass) or a list of violation records. The kernel validates this interface at load time. This is the extensibility mechanism: guidebooks are not just constraint libraries; they are pluggable domain packages. 2.3 Formal Definition Definition 1 (Nidus System 1 ).S = (R,A,D,W,F,T ,Π,Σ,Λ,G)where:R 2 requirements, A = (C,E)34architecture (components + connectors),D5design elements,W6workflows (FSMs with QF_LIA guards),F7features (scope + delivery status),T8trace links,Π9proof obligations,Σ = (K,L)1012coordination state (claims + friction ledger),Λlessons (failure→ root-cause→ obligation; see Section 7), G 11guidebook hierarchy. Definition 2 (Trace Link 8 ).t = (r,c,d): requirementr ∈ R, componentc∈ C, design element d∈ D∪W . Property 1 (Decidability and Complexity 69 ). All sets are finite; workflow guards are QF_LIA/QF_IDL [4]. Obligations decompose into three decidable categories: (a) finite graph checks (traceability, orphans, DAG acyclicity): O(|C|+|E|+|T|), (b) schema checks (field completeness): O(|F|), (c) bounded arithmetic over workflow guards, decided by Z3 in time polynomial in the number of guard variables (fixed per workflow). Total verification cost per mutation:O(|Π|·|S|)where|S|is the total number of entries across all artifact sections, linear in artifact size for each obligation. Definition 3 (Immutable Obligations). A proof obligationπwith(immutable t)belongs toΠ imm ⊆ Π. Mutations that remove or weaken anyπ ∈Π imm are rejected. Theorem 2 depends on this: Π imm 0 ⊆Π n for all accepted histories. Definition 4 (Trust Tier12).tier(a,L) = unrestrictediffric(a,L,w) < θ 1 ;supervisedifθ 1 ≤ fric < θ 2 ; restricted if fric≥ θ 2 . Restricted agents cannot claim features. Clean deliveries earn promotion. Definition 5 (Guidebook Hierarchy11).G = (G 1 ,... ,G m ): constraint bundles imported tran- sitively. EachG i declares SMT formulas compiled to Z3 assertions. Inheritance is monotonic: Π(G parent )⊆Π(G child ). Definition 6 (Governance Loop91012). (1) Agent observesS. (2) Proposes mutationm. (3) Kernel evaluatesmagainst allπ ∈Π: pass→persist +probe_success; fail→reject +agent_rejection+ UNSAT core (the minimal subset of constraints that caused the failure). (4) Tier recomputed. 6 Living S-Expression (Nidus) Human (Architect) LLM (Collaborator) SMT Solver (Verifier) Implementation Code (C++, Rust, TS, Py) Documentation (Markdown, Audit) Domain Artifacts (HDL, BIM, ...) ... IDE/Editor MCP Tools SMT-LIB2 Natural Lang generates anchors anchors anchors Figure 1: Representational closure. Human, LLM, and Solver read/write the same S-expression. 3 The Verification Kernel Guidebook constraint compilation. Guidebook constraints (Listing 2) have two enforcement paths. Apo-kindfield binds to an evaluator function registered in the kernel’s dispatch table— evaluators are not hardcoded; guidebook modules can register new evaluator functions at import time (Section 2), extending the kernel without modifying it; the evaluator traverses artifact sections and returns violations. Az3_formulafield is compiled to a native Z3 assertion: propositional variables are declared as Z3 Booleans, operators map to their SMT-LIB2 equivalents, and the assertion is checked for satisfiability. Internally inconsistent formulas (e.g.(and p (not p))) are flagged as UNSAT at import time. The compilation is mechanical—the S-expression grammar is a strict subset of SMT-LIB2. Propositional variables map to artifact predicates:feature_deliveredis true when any feature’s status equalsdelivered;has_test_pathsis true when its scope contains atest-pathsfield. The evaluator computes these predicates from the artifact state before each Z3 call. Obligation taxonomy.Proof obligations span seven categories: structural, schema, SMT, temporal, anti-theater, coverage, and domain (including hardware-specific kinds: clock-domain crossing, port- width consistency). Guards compile to SMT-LIB2 with minimal translation overhead; Z3 [2] consumes them directly. Graph checks areO(|V| +|E|)whereVis the set of components andEthe set of connectors in the architecture; SMT queries over QF_LIA with fixed variable counts. Failed mutations return an UNSAT core; verified_repair_search returns only proven fixes. what_if applies a proposed mutation to an in-memory copy of the artifact, runs all proof 7 obligations against the copy, and discards it—the agent receives a pass/fail verdict and any UNSAT core without risking state corruption or accumulating friction. Agents usewhat_ifto explore the constraint landscape at zero risk. Monotonic invariants ensure requirement count, PO count, and delivered status can never decrease. The artifact is a single object—rather than a distributed collection of files—because representational closure (Section 2.1) requires that human, LLM, and solver all read the same structure; splitting it would reintroduce the fragmentation the design eliminates. Git is the artifact’s write-ahead log. Verification before persistence.The practical consequence is that no other agent or tool ever observes a state that fails the active verification gate. In conventional CI/CD, a broken commit exists on the branch—other agents may pull it, build on it, or reference it before the pipeline reports a failure. Nidus eliminates this window: the daemon verifies the mutation in memory and only then appends it to the git write-ahead log. The repository contains exclusively states that have passed the active verification gate. Theorem 2 formalizes this: every persistedS i satisfiesΠ i . Verification is sound with respect to the currently encoded obligation set and trusted evaluators, but does not guarantee properties that have not been modeled. A proof obligation that runs the feature’s test suite during delivery extends this guarantee to the code: nothing ships unless it compiles and passes. Kleppmann [17] predicts that AI will make formal verification mainstream; Nidus is an instance. LLM Agent (any MCP client) read_system commit_mutation verify_mutation Nidus MCP Server Living Artifact S-Expression Store SMT Solver QF_LIA / QF_IDL 0 1 2 fetch SMT-LIB2 persist pass? Figure 2: MCP server: read (step 0), verify (step 1), commit (step 2). Commit is gated on verification. 3.1 Formal Guarantees The following properties are straightforward by construction, but we state them explicitly because the rest of the paper refers to them as contracts. Theorem 1 (Decidable Verification). For anySand mutationm, verification ofmagainstΠ terminates in bounded time. Proof. All sets finite (Def. 1); graph checks O(|V| +|E|); guards QF_LIA (decidable);Π finite. Theorem 2 (Incremental Correctness). IfS 0 satisfiesΠ 0 and mutationsm 1 ,... ,m n are accepted, then everyS i satisfiesΠ i andΠ imm 0 ⊆Π n . Proof. Induction. Accept only ifS i satisfies all π ∈Π i . Immutable POs cannot be removed. 8 Theorem 3 (Monotonic Governance). Under guidebook hierarchyG, accepted child mutations satisfy all parent obligations. Proof.Π(G parent )⊆Π(G child ). Child verification checks all. Theorem 4 (Engineering Record Completeness). If the artifact historyH = (S 0 ,m 1 ,... ,m n ,S n ) satisfies Theorem 2 and each accepted mutation carries an attestation (feature, agent, verification re- sult, fingerprint transition), then compliance certificates, traceability matrices, and impact analyses are derivable as projections of H without external state. Proof.EachS i contains all requirements, traces, proof obligations, evidence, and coordination entries (Definition 1). Each attestation records provenance.His totally ordered by git. Any required report is a query over H . Theorem 2 guarantees that no accepted mutation violates the current PO set. This eliminates regressions that the PO set captures. Semantic defects not encoded as POs—performance regressions, emergent cross-artifact invariants, specification errors in the POs themselves—are not blocked. The surface is sound but not complete; its coverage grows as the architect crystallizes new obligations from observed failures. We callΠ∪Π(G)∪monotonic ratchetsthe constraint surface: the union of artifact proof obligations, inherited guidebook constraints, and the invariants that prevent requirement/PO count from decreasing. The surface is decidable (Theorem 1), preserves correctness (Theorem 2), and composes monotonically across organizations (Theorem 3). Remark (Computational Separation). Nidus is the bounded half of a Turing-complete system. The proposer (LLM) explores an unbounded search space; the kernel gates every persistent transition through finite, terminating verification. This separation means that adding agents does not increase verification cost, and when the model changes, the constraint surface remains sound. 4 Recursive Self-Governance Definition 7 (Recursive Self-Governance). A Nidus system exhibits recursive self-governance if mutations toΠ are themselves subject to verification byΠ. ACL2 [5] does not re-check theorem database changes; seL4 [8] requires human-guided Is- abelle/HOL; Cedar [3] analyzes policies but is not itself a policy. Nidus: governance rules live in the same artifact as governed content, every mutation—including toΠ—passes through the same automatic gate. PO-CONFORMANCEverifies artifact structure;(immutable t)POs block removal. TCB: the kernel evaluator. Governed surface: the entire artifact. Section 9 reports the empirical test: add PO, violate it, attempt removal. Runtime self-governance. Recursive self-governance extends to the runtime itself. The kernel evaluates proof obligations not only on the artifact but on its own process state: a memory-ceiling PO rejects commits when heap usage exceeds a configurable threshold (derived from the 160 GB OOM crashes in Section 7), a latency-bound PO flags verification times exceeding 5 s, and a state- freshness PO detects when the in-memory artifact has diverged from the WAL. These are ordinary proof obligations in the artifact—an agent can read them, and the kernel enforces them on itself. Relative to the systems reviewed here (Section 8), we are not aware of another architecture that represents runtime self-constraints as first-class artifact obligations enforced by the same mutation gate. 9 Autonomic evolution.The decay detector is a background process that scans the friction ledger for recurring failures, grouped by PO kind (e.g. repeatedtraceability-completerejections). When a particular PO-kind’s failure count exceeds a configurable threshold within a rolling window, the system generates a candidate proof obligation, tests it viawhat_ifagainst the current artifact, and deposits it as an open feature for an agent to commit. Concrete instance: agents submitted features with empty scopes. The system generatedPO-DELIVERY-CASCADE—a proof obligation that rejects any feature delivery whose scope lacks at least one requirement, one code-path, and one test-path—verified it, and an agent committed it. The vulnerability is permanently closed. 5 Stigmergic Multi-Agent Coordination Friction accumulates unevenly—not because one agent is worse, but because its trajectory diverged into a constraint-dense neighborhood. Trust tiers, derived as a pure function over the ledger’s rolling window, route unproductive trajectories toward uncontested work. This is a throughput mechanism, not a quality judgment—mirroring ant colony reallocation [9]: the ledger is the pheromone; the tier gate is the pivot. P(success) for each (agent, feature) pair cross-references per-PO-kind reputation vectors against scope-implied PO requirements. An agent with high traceability accuracy but low evidence accuracy is routed to traceability-heavy features—not gated entirely. Multi-level identity: session (CAS), family (blind spot detection), trajectory (routing). Success templates from other families are surfaced in workbenches; pre-flight warnings fire on historically failed PO kinds. When multiple agents contribute to the same area, collaborative credit accrues to all contributors—the game rewards cooperation, not competition. 6 Proximal Spec Reinforcement (PSR) Section 1 argued that engineering invariants require external enforcement. PSR is the mechanism. The V-model chain—requirements→architecture→design→traces→proofs→evidence—lives in the verified artifact, not in model parameters. When verification fails, the kernel returns an UNSAT core—the minimal subset of proof obligations whose conjunction makes the proposed state unsatisfiable—which tells the agent exactly which link in the engineering chain broke. The friction tier constrains which features the agent may attempt next. Human engineering teams succeed because the environment—architectural plans, requirements, design decisions—constrains what individuals produce. AI agents without a persistent engineering context have no plan to be better toward. RL [14] makes each generation better; PSR gives it direction. The architect’s contribution is that direction: not just proof obligations (what must hold) but architecture decisions (how to structure it), design elements (what abstractions to use), and the development vector (what to build next). Guidebooks are organizational knowledge—crystallized from architectural judgment, inherited by every project that imports them. The constraint surface is the reward model—but decidable, explicit, and persistent across sessions and model generations. In practice, agents from all three families produced verified deliveries within their first session— the UNSAT core narrowed the search space on each rejection, providing the equivalent of a curriculum without any prior training on the artifact’s structure. The mapping to reinforcement learning is structural: 10 Agent α (unrestricted) Agent β (unrestricted) Nidus Kernel (verify + commit) Living Artifact (S, Σ, Λ, L) Z3 Solver Exploration (no friction) what_if(change_set) copy-tree(root-form) verify(mutated-copy, all Π) would_pass=true would_pass, discard copy (no friction) Commit (state transition) claim_slice(FEAT-X, α) Σ.F += (α, FEAT-X, t_exp) commit_change_set(mutations, fingerprint) CAS check + verify(all Π) PASS persist + L += probe_success(α) committed (new fingerprint) Perturbation cascade commit_change_set(mutations, STALE fp) CAS CONFLICT (fingerprint mismatch) commit_change_set(bad mutation, fresh fp) verify(all Π) FAIL: PO-TRACE-01 violated L += (rejection, β, t, FEAT-Y) REJECTED + UNSAT core Tier effect my_workbench(β) τ(β, L) = fric ≥ θ₁ tier=supervised, routing=restricted, simpler work only what_if: pure exploration, no state change, no friction commit: state transition, CAS check, friction recording τ(a,L): deterministic tier derivation from rolling window Figure 3: Stigmergic dynamics. Phase 1: speculative exploration. Phase 2: verified commit. Phase 3: rejection + UNSAT core. Phase 4: tier narrowing. No orchestrator. 11 RL conceptNidus mechanism Reward signal what_if returns accept/reject + UNSAT core before persistence Reward shapingFriction score: sum of per-PO-kind failure weights (graded, not binary pass/fail) Policy gradientRepair templates from UNSAT cores: concrete S-expression fixes Value functionPer-PO-kind reputation vectors route agents to their strengths CurriculumPre-flight PO-kind warnings before claiming; scope-implied difficulty Environment designGuidebooks: inherited organizational knowledge, persistent across sessions The game is cooperative: each agent’s successful delivery strengthens the artifact that all agents share, and no agent benefits from another’s failure. Formally, letu i (S)be the expected success rate of agention artifact stateS. When agentjdelivers featuref, the artifact gains traces, evidence, and coverage:S ′ ⊇S(monotonic ratchets prevent removal). Since more traces reduce traceability-completerejections for all agents,u i (S ′ ) ≥ u i (S)—satisfying the condition for a team game in the sense of Marschak (1955). Better feedback (graded friction, per-kind routing, concrete repair examples from UNSAT cores) produces faster convergence. The specification is the reward function. RLVR [14] shapes the model during training; PSR shapes the environment at inference time. The two are complementary. The model does not need to be brilliant; it needs to be checkable. Proxy stigmergy.Smaller models (e.g. Haiku-class, Codex-mini) cannot hold the full governance protocol in context. In practice, a coordinator agent—running a larger model—claims a feature, decomposes it into focused subtasks, and dispatches each subtask to a cheaper subagent with a narrowed context containing only the relevant requirements, design elements, and PO subset. The subagent proposes mutations; the coordinator submits them through the kernel. The verification floor catches errors from either party: if the coordinator’s decomposition misses a trace, the PO rejects the delivery regardless of which agent produced it. This pattern reduces token cost by 60–80% on routine deliveries while preserving the governance guarantee. 7 Enforcement Mechanisms If agents can fabricate evidence, the substrate degenerates into security theater. The attack.During development, an agent submitted fabricated evidence—witness="governance-audit" and status=passed—for features it had never tested. The defense. Three structural mechanisms compose: 1.Witness allow-list. Evidence is rejected unless the witness field matches a registered source (e.g. kernel-test-gate, ci-pipeline, human-review). 2.Test-execution hash. Every evidence form includes a SHA-256 digest of test file contents, computed server-side—agents never touch the hash. 3. Fused execution.run_evidence_gateruns tests, computes hash, and submits evidence atomically. You cannot submit evidence without running the tests. Theevidence-provenancePO verifies conditions 1–2 at commit time. Theclaim-before-dispatch PO intercepts unclaimed work at the mutation layer—no transport can bypass it. 12 Threat model assumptions. These defenses hold under: (a) the kernel is not compromised (the daemon is the TCB); (b) test runners are honest (a compromised runner could produce valid hashes for non-running tests); (c) guidebook authors are trusted (a malicious guidebook could weaken constraints). Nidus does not claim security against adversarial kernel modification or colluding insiders—it prevents the common case: agents optimizing for speed by fabricating evidence. The obligation argument.Before the gate, agents faced ambiguity: fabricate (fast, zero value) or test (slow, real value). After, the only path that succeeds produces real evidence. For example, the evidence-provenanceconstraint (PO-kindevidence-provenance, Listing 2) rejects any evidence whose witness is not in the allow-list or whose hash is missing—so the only mutation that passes is one produced by the fusedrun_evidence_gatetool. The architect eliminated the ambiguity by adding this constraint; the agents benefited from the narrower search space. This pattern repeated across all obligations: each constraint, crystallized from the architect’s steering, removes a class of unproductive agent behavior. Retroactive verification.retroactive_verifyevaluates candidate POs againstNhistorical states from the Git WAL, returningsafeorover-constrained. This is bounded model checking over the mutation history. Incremental verification.Full verification is too slow for interactive commits. The solution: map each mutation’s target section to the PO kinds at risk. A commit touching onlyfeaturesskips irrelevant kinds. MCP stdio processes delegate to a single TCP daemon with cached solver state, keeping agent-facing latency sub-second. Two-mode verification.Analysis of the proof obligation evaluators revealed that all commit-path checks evaluate formulas where variables are already bound from artifact state—no constraint solving is needed. The system operates in two modes. Online mode: every commit is verified by direct Lisp evaluation on ground artifact state, sub-millisecond, no solver dependency. Guidebook management mode: when an architect authors, imports, or composes guidebook constraints, Z3 validates the constraint set for mutual consistency—genuine satisfiability checking with free variables. The SMT solver is a guidebook compiler’s tool, not a commit-path dependency. S- expressions remain SMT-LIB2; the representation supports solver use. The runtime rarely needs it. Thin MCP relay. A practical constraint on multi-agent deployment is per-connection memory. Each MCP client (Claude, Gemini, Codex) spawns an MCP stdio process. Originally, each loaded the full daemon codebase (926 MB), limiting concurrent agents to∼3 on a 4 GB server. Since tools/callalready relays to a shared TCP daemon, the MCP stdio process was reduced to a pure JSON-RPC relay (15 MB), enabling∼60 concurrent agent connections—a prerequisite for the investigative swarm described next. Investigative swarm.The daemon decomposes audit queries into self-contained jobs, each inlin- ing relevant artifact context (requirement text, feature scope). Cheap agents (e.g. 100 parallel Jules sessions, Google’s Gemini-based coding agent) investigate in review mode—reading code, judging consistency, reporting structured findings. Findings are ingested into the coordination section; a proof obligation ensures all mismatches are resolved. The constraint surface grows from stochastic exploration, not just architect observation. 13 SOP enforcement through gate-sequence POs. Standard operating procedures are documents that agents consult when convenient and skip when optimizing for speed. An FPGA synthesis agent repeatedly skipped pre-synthesis gates (lint, simulation, resource model verification), wasting $100–150 per failed synthesis run on cloud infrastructure. The agent’s self-assessment: “I optimize for speed over correctness. The SOP exists because this exact behavior wasted money.” The fix encodes the SOP as a gate-sequence proof obligation with DAG dependencies. Each gate declares an identifier, a required witness type, and a list of prerequisite gates: (gate FI-1 (description "Pre-synth") (witness "verilator-sim") (depends-on FI-0 FI-0b FI-0c)) The evaluator checks coordination evidence entries for each gate in the dependency order. If gate FI-0c (formal verification) has no evidence, the delivery is rejected: “feature FEAT-X gate FI-1 requires FI-0c to pass first.” The agent cannot skip gates because the constraint surface does not offer a path that avoids them. This transforms SOPs from behavioral aspirations into structural properties of the engineering environment. Lesson provenance: the artifact’s immune system. Proof obligations are positive constraints: what must hold. Lessons are negative constraints: what must not happen. Together they complete the constraint surface. During a 12-hour session, the daemon crashed six times from unbounded memory growth— each a different manifestation of the same class of bug. Each crash was debugged, fixed, and committed. The commit messages encoded the diagnostic chains, but commit messages die with the session. The next agent would rediscover the same failures because the failure-to-obligation chain lived in git, not the artifact. The fix: alessonssection in the artifact (Λin Definition 1). Each lesson links a failure to a root cause to the obligation that prevents recurrence: (lesson LSN-OOM-Z3-PER-FEATURE (failure "160GB OOM: Z3 called per feature x constraint") (root-cause "Constraint satisfiability is guidebook-level") (fix "Removed per-feature Z3 loop") (obligation "skip-guidebooks at commit time") (affected-scope "lisp/epochd-proof-guidebook.lisp") (cost "160GB OOM, 4 daemon crashes") (commits "ce3e50d" "2d721")) Each lesson is a negative proof obligation. Z3 can verify soundness: the lesson’sroot-cause field identifies the precondition (here: “Z3 called per feature×constraint”), and theobligation field names the invariant that prevents it (here: “skip-guidebooks at commit time”). The encod- ing is(implies precondition failure)and(implies context (not precondition)). Con- cretely, for the lesson above:precondition≡ (and commit-path-mode (z3-called-per-feature true)) ; the obligation asserts(implies commit-path-mode (not (z3-called-per-feature true))). Z3 checks whether the conjunction is satisfiable. If UNSAT, the obligation provably prevents the failure. If SAT, there is a path the fix does not cover. The workbench surfaces lessons whoseaffected-scopeoverlaps the agent’s feature code- paths—not by keyword matching but by formal scope intersection. An agent editing the verification pipeline sees the OOM lessons before writing code. Institutional knowledge becomes a structural property of the artifact, not a behavioral property of agents who happened to read the right commit messages. 14 From a game-theoretic perspective, lessons solve the tragedy-of-the-commons on institutional knowledge. The mechanism: recording a lesson is a public good (all future agents benefit from the narrower failure surface), while the cost falls on the recording agent (time spent diagnosing and formalizing). Nidus aligns incentives by awarding reputation credit proportional to the lesson’s severity—agents that crystallize high-cost failures earn faster tier promotion. The game rewards knowledge crystallization alongside feature delivery. The system becomes antifragile: each failure strengthens the constraint surface. 8 Related Work LLM-assisted formal verification.Mugnier et al. [6] (Laurel) use LLMs to generate Dafny helper assertions that unblock SMT-backed verification—an “unbounded prover, bounded verifier” split structurally similar to Nidus. The difference: Laurel generates assertions for a fixed program; Nidus governs the co-evolution of the specification itself, including its proof obligations, through the same decidable surface. Hao et al. [7] formalize natural-language constraints into SAT/SMT with UNSAT-core repair loops—close to Nidus’swhat_if+ repair mechanism. Their framework governs plans; Nidus governs the full engineering artifact (requirements, architecture, design, traces, proofs, evidence) as a singleton. Kleppmann [17] predicts that AI will make formal verification mainstream by removing the proof-writing bottleneck; Nidus is an existence proof of that thesis, applied to engineering governance rather than program correctness. Agent frameworks and planning layers.Agent-first IDEs generate implementation plans before coding; multi-agent frameworks (AutoGen [13], SpecMAS [10]) add orchestration and protocol verification. These are complementary to Nidus, which occupies a different layer: not an agent framework but a governance substrate beneath any framework. Agents from any family connect via MCP; the surface gates all of them identically. RLVR and process reward models can coexist with the surface—the model improves its adherence during training; the surface guarantees enforcement at inference time. Formal methods and MBSE.Proof-carrying code [5] established the “unbounded prover, bounded verifier ” architecture decades ago; Nidus is the LLM-era realization applied to engineering artifacts rather than machine code. ACL2 does not re-check its theorem database on modification; seL4 [8] requires human-guided Isabelle/HOL. Cedar [3] analyzes authorization policies but is not itself governed by its policies. The MBSE+SMT patent [15] translates MBSE artifacts into first-order logic via a translation layer. Unlike such approaches, Nidus keeps the artifact solver-aligned: the same S-expression structure is used for storage, inspection, and constraint compilation. TLA+, Dafny, and Lean/Coq/Isabelle verify programs in a proof language separate from the program; Nidus’s representational closure means the specification, the database, and the solver input are the same object. Normative multi-agent systems.The normative MAS tradition [18] separates an organizational norm layer from domain agents, with enforcement components that detect violations—structurally close to Nidus’s constraint surface. Guidebook inheritance (Π(G parent )⊆Π(G child )) parallels hier- archical institutional norms in which lower-level organizations inherit constraints from higher-level ones [20]. Nidus adds SMT-decidability, representational closure, and recursive self-governance to this pattern. 15 Executable specifications and MBSE. SysML v2 [19] moves model-based systems engineer- ing toward executable, textual specifications—structurally converging with Nidus’s artifact-as- specification. The difference: SysML v2 models are authored by humans and verified by tools; Nidus artifacts are co-authored by humans and LLMs and verified on every mutation. SysML v2 has no recursive self-governance, no friction-based coordination, and no mechanism to prevent governance theater. Self-modifying systems. The Gödel Machine [12] gates self-modification on proof but is a theo- retical framework over unrestricted logic. Nidus restricts to decidable tuples (finite sets, QF_LIA guards) for tractability, making recursive self-governance practically enforceable. 9 Evaluation We evaluate four claims: (C1) the constraint surface prevents regressions; (C2) guidebook in- heritance works across projects; (C3) recursive self-governance holds; (C4) the friction model differentiates agent behavior. All experiments run on the self-hosting deployment—the system that governed its own construction. 9.1 C1: Constraint Surface Prevents Regressions Lesion study. For each of the 49 removable elements in a sandbox artifact, we removed the element via commit_change_set and recorded whether verification rejected the mutation. Table 1: PO coverage by element type (N = 49 removals). Element typeNGuardedRateGuardian PO kind Trace1111100%traceability-complete Component66100%connector-integrity Design element66100%feature-scope-valid Requirement11982%feature-scope-valid Connector500%gap (subsequently closed) Proof obligation1000%sandbox lacked immutable flag Total493265% Two gaps found. The connector gap led toconnector-existence, implemented through the governance loop—the experiment identified the weakness; the fix was delivered by the mechanism it now protects. The PO gap was a sandbox limitation: the production artifact uses(immutable t) to protect POs from removal. Verification latency. Table 2 reports wall-clock times for the production artifact (461 features, 873 requirements, 238 POs). The daemon maintains cached solver state; all measurements include TCP round-trip. Incremental verification (the commit-path hot loop) runs under 500 ms. Full health checks run under 2 s. Both scale linearly with PO count; the current 238 POs leave headroom for growth. 16 Table 2: Verification latency on the production artifact (M4 Mac Studio, SBCL 2.6, 238 POs). OperationWall-clockNotes ping1 msDaemon heartbeat read_system173 msFull artifact + traceability matrix precommit-check493 msIncremental: 238 POs, touched sections only artifact_health∼2 sFull: all POs + governance health score commit_change_set2–5 sVerify + CAS + git commit + WAL push 9.2 C2: Guidebook Inheritance This claim is trivially guaranteed by the monotonic inheritance semantics (Theorem 3), so the evaluation serves as a validation rather than an experiment. The production deployment uses twelve guidebooks (128 constraints) across four layers: corporate (copyright, singleton, daemon authority—10 constraints), engineering (module DAG, function granularity, file size, naming, spec- first, TDD—37 constraints), compliance (EU AI Act, ISO 27001, ISO 42001, NIST AI RMF, DO-178C, SOC 2, HIPAA, Singapore MGF—72 constraints across eight frameworks), and domain (chip-design RTL governance—9 constraints). Five governed projects inherit from the same guidebook hierarchy. A data-loss-prevention project importing the corporate and EU AI Act guidebooks was rejected for missingtest-pathson delivery—a constraint it never defined locally. The organizational standard was enforced mechanically, confirming the implementation matches Theorem 3. 9.3 C3: Recursive Self-Governance Three mutations on the sandbox, in sequence: (1) Add PO with(immutable t)—accepted; PO immediately active. (2) Submit requirement violating the new PO—rejected by the PO just added. (3) Remove the immutable PO—rejected. The system accepted an addition to its own constraint surface, enforced it on the next mutation, and blocked its removal. 9.4 C4: Friction Differentiates Agent Behavior 125 friction events, 25 agent sessions, three model families. Gemini sessions: predominantly rejections (44/47 events). Codex sessions: proportionally more abandonments (odds ratio= 5.04, Fisher ’s exactp = 0.02). Seven sessions reached restricted tier; the highest-friction session (36 events) was mechanically gated from claiming features. Different model families produce different failure signatures; the friction model routes accordingly. 9.5 Architect-Designed Constraints Table 3 shows five constraints crystallized from the architect’s steering during construction. Each row traces observed friction to a deployed constraint to the class of agent behavior eliminated. Threats. (1) All deployments internal to one organization. (2) Coverage gaps found and closed during self-hosting (connector, evidence, dispatch). (3) Swarm experiment ran seconds, not hours. (4) A third deployment (SystemVerilog, 68 RTL modules) is bootstrapped but not yet independently operated. Future work: independent replication on an external codebase andk-step forward reachability experiments. 17 Table 3: Architect-steered constraints. Observed friction→crystallized obligation→agent behavior eliminated. FrictionConstraintBehavior blocked 78 fabricated evi- dence incidents (implies evidence_submitted (and witness_registered hash_present)) Unregistered witness or miss- ing hash Unclaimeddis- patch (implies work_dispatched feature_claimed_by_agent) Work on unclaimed features Deliverywithout tests (implies feature_delivered (and has_code_paths has_test_paths ...)) Incomplete scope Backfilled specs (temporal true) (po-kind spec-precedes-code) Spec committed after code DAG violations (and (not parse_imports_query) (not mutate_imports_query) ...) Module back-edges 10 Conclusion LLM agents generate code. They do not enforce engineering invariants. Nidus combines a fast proposer (LLMs) with a constraint surface that verifies every mutation. The practical result: guide- books encode organizational standards inherited by every governed project; the surface compounds as each obligation permanently eliminates a class of unengineered output. The verification-gated history is a complete engineering record with respect to the modeled artifact and active obligations (Theorem 4): compliance certificates, traceability matrices, and impact analyses are projections—the audit trail is a theorem, not a process. LLM agents replace coders. They do not replace the architect. Requirements, architecture decisions, and the development vector remain human input. The surface outlives the agents, the models, and the frameworks. When the next model generation arrives, the constraints remain sound. When Nidus itself evolves—new PO kinds, new guidebook constraints, new sections—the evolution is governed by the same surface. Each commit carries a daemon-generated attestation: which feature, which agent, which verification result, which fingerprint transition. The git write-ahead log is a sequence of verified, attributed governance states—a formal development in the mathematical sense. As models improve, the architect’s role itself becomes partially automatable: decomposing features, drafting architecture decisions, proposing proof obligations from friction patterns. The living artifact makes this transition safe because the mechanical architect (the constraint surface + Z3) is separated from the creative architect (the human or LLM making judgments). Whoever proposes—human or model—the surface verifies. The creative role can migrate gradually from human to LLM without the governance degrading, because the governance is a property of the artifact, not of who writes to it. k-step forward reachability—verifying that no sequence ofklegal mutations can reach a state violating an immutable obligation, a bounded model checking problem over the constraint surface— and independent replication on an external codebase complete the agenda. Acknowledgements. I thank Anton Afanasyev for discussions that improved the clarity of this paper. 18 Disclosure. The recursive self-governance mechanism is the subject of Swiss patent application CH000371/2026 (filed with IGE). References [1] J. McCarthy, “Recursive Functions of Symbolic Expressions,” CACM, 3(4), 1960. [2] L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” TACAS, LNCS 4963, 2008. [3] J. Cutler et al., “Cedar,” OOPSLA, 2024. [4] C. Barrett, P. Fontaine, C. Tinelli, “SMT-LIB Standard v2.6,” 2017. [5] M. Kaufmann, P. Manolios, J. S. Moore, Computer-Aided Reasoning, Kluwer, 2000. [6]L. Mugnier et al., “Laurel: Unblocking Automated Verification with Large Language Models,” arXiv:2405.16792, 2024. [7] Y. Hao et al., “Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools,” NAACL, 2025. arXiv:2404.11891. [8] G. Klein et al., “seL4: Formal Verification of an OS Kernel,” SOSP, 2009. [9] G. Theraulaz and E. Bonabeau, “A Brief History of Stigmergy,” Artificial Life, 5(2), 1999. [10] F. Hahn et al., “SpecMAS,” arXiv:2408.00230, 2024. [11] C. Wolf, “SymbiYosys: Formal Verification with Yosys,” 2018.https://github.com/YosysHQ/ sby [12] J. Schmidhuber, “Gödel Machines,” AGI, 2003. [13] Q. Wu et al., “AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation,” COLM, 2024. arXiv:2308.08155. [14] H. Lightman et al., “Let’s Verify Step by Step,” ICLR, 2024. [15] “Verification of Model-Based Systems Engineering Artifacts,” WO2022231594A1, 2022. [16]CodeRabbit, “State of AI vs. Human Code Generation,” December 2025.https://w. coderabbit.ai/whitepapers/state-of-AI-vs-human-code-generation-report [17]M. Kleppmann, “AI will make formal verification go mainstream,” December 2025.https: //martin.kleppmann.com/2025/12/08/ai-formal-verification.html [18]O. Boissier et al., “A Framework for Normative Multi-Agent Organisations,” Dagstuhl Seminar Proceedings, 09121, 2009. [19]Object Management Group, “OMG Systems Modeling Language (SysML) v2.0,” 2025.https: //w.omg.org/spec/SysML/2.0 [20] L. van der Torre et al., “Five Guidelines for Normative Multiagent Systems,” JURIX, 2009. 19

Instant research discovery