Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale

arXiv:2611.02285v1 [cs.SE] 1 Nov 2026

Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale Author: Jason Hickey Affiliation: Independent Research∗ Email: jasonh@gmail.com

Abstract When autonomous coding agents synthesize implementation code, formal specifications, and mechanical proofs simultaneously, the software engineering hierarchy inverts: the formal specification becomes the primary human-reviewed artifact, while source code and proof scripts become disposable build outputs. This paper presents an end-to-end architecture for agentauthored, formally verified software engineering. First, we establish a logic-agnostic foundation combining a spec-first stack inversion, a zero-code-review workflow gated by automated continuous integration (CI) checks, and a minimal Verification Intermediate Representation (VIR) lowered via a thin, verified translator. Second, we pair an extensional Computational Type Theory (CTT) specification layer with Higher-Order Abstract Syntax (HOAS) and linear resource typing in the VIR—eliminating rewrite friction for synthesis agents while defining an experiment, its protocol frozen before the first reader, to measure whether removing boundary coercions improves human specification readability. Third, we scale collaboration across multi-team organizations using Personal Spec-Copilots and a Shared Synthesis Fleet that detects cross-team Semantic Merge Conflicts and fuses modular contracts into zero-copy binaries. We illustrate this architecture on a zero-copy authenticated message router and distinguish our existing empirical baselines (salt, SaltBench, x86lean, and MetaPRL) from newly proposed components.

1. Introduction For seventy years, much of the software stack—programming languages, optimizing compilers, software design patterns, and code review workflows—has been shaped around one scarce resource: human attention. • Programming Languages: Mainstream languages introduced complex syntactic sugar, implicit type coercions, operator overloading, and intricate lifetime elision rules largely for the convenience of human readers and writers. • Optimizing Compilers: Production toolchains such as LLVM [37] and GCC grew into large, unverified heuristic engines so that human engineers could write clean, readable, textbook code and still obtain high-performance machine binaries. ∗

Disclaimer: The author is employed by Google Research. The views in this paper are of the author and do not necessarily reflect the views of his employer, or any employer.

1

• Software Architecture: Engineering practices enforced strict module indirection, deep objectoriented hierarchies, and “Don’t Repeat Yourself” (DRY) boundaries so that a human developer could modify one subsystem without inadvertently breaking another. With the rise of capable coding agents, this historical constraint has inverted: code generation is now cheap and abundant, and we take as our premise that human review, not generation, is now the bottleneck. Asking a senior software engineer (SWE) to manually audit 5,000 lines of agent-generated Rust or C++ for subtle memory bugs, race conditions, or security vulnerabilities is slow, exhausting, and error-prone. However, when a coding agent generates a formal proof alongside its implementation—and a small, mathematically trusted proof kernel [4] mechanically verifies that the implementation satisfies a 25-line formal specification—the economics of software review change fundamentally. Human engineers no longer need to inspect how the implementation works or how the proof was constructed. Instead, engineering rigor concentrates on a much smaller, higher-leverage surface: verifying that the formal specification accurately captures intended system behavior.

1.1 The Five Architectural Pillars This paper proposes an end-to-end architecture structured around five pillars: • The Core Inversion (Spec as Source of Truth): In greenfield development where AI agents synthesize implementation code, formal specifications, and mechanical proofs, the specification becomes the primary human-authored and human-reviewed artifact, while implementation code and proof scripts are treated as ephemeral build outputs regenerated on demand. • Zero Human Code Review: SWEs no longer read implementation diffs or proof scripts during change review; human attention is strictly conserved for module boundary specifications and automated operational telemetry (latency benchmarks, memory profiles, and automated vacuity and mutation gates). • Shrinking the Compiler TCB via a Verification IR (VIR): Once humans stop reading source code, languages no longer require human-ergonomic syntactic sugar or massive unverified optimizing compilers, converging instead toward a Verification IR (VIR) where agents perform aggressive optimizations directly in verified source and lower via a thin, CompCert-style verified translator [42]. • Designing for Readability and Rewrite Ergonomics (Extensional CTT + HOAS): Pairing an extensional Computational Type Theory (CTT, pioneered by the Nuprl/MetaPRL family of provers [13, 24]) with Higher-Order Abstract Syntax (HOAS) [50] removes rewrite friction (“transport hell” and binder-renaming boilerplate) for synthesis agents and removes coercions at module boundaries for human reviewers. • Organizational Scaling via a Two-Tier Agent Fleet: Across teams and open-source communities, SWEs collaborate on a modular specification graph using lightweight Personal Spec-Copilots backed by a Shared Synthesis Fleet that detects cross-team Semantic Merge Conflicts early and compiles modular contracts into globally fused machine code.

1.2 Goals and Explicit Non-Goals To turn source-level agentic verification into a practical engineering discipline at organizational scale, our architecture targets four primary goals: 2

• Minimize Human Review Attention (Estimated >90% Reduction): Restrict human change-review surfaces strictly to public module boundary specifications and automated nonfunctional telemetry, eliminating manual line-by-line code review for verified modules. While the 90% figure is an estimate, its first measurement is commissioned via the review-surface ratio (specification lines vs. implementation and proof lines) over the 181 conditions of record in SaltBench’s pilot matrix, declared as a proxy for attention. The synthesis cost alongside this saving is already measured: on five Rust systems components refereed by a withheld test suite, asking the agent to specify and verify its own code cost more on all five, by a practical margin: no premium exceeded 2.8879× and the three cheapest sat below 1.4× (one model, three runs per condition), a bound of this population and not a promise about larger ones [26]. • Shrink the Compiler Trusted Computing Base (TCB): Move complex, bug-prone [60] program optimizations out of unverified compiler passes (such as LLVM) and into agent-generated, source-verified transformations over a dedicated VIR. • Maximize Specification Readability and Agent Ergonomics: Keep formal specifications mathematically clean, concise, and readable by generalist SWEs—free of proof witnesses, artificial termination fuel, or index-shifting plumbing—while minimizing proof-search friction for the agent. • Scale Multi-SWE Collaboration: Establish an organizational workflow where independent engineering teams compose modular specifications safely and detect logical contradictions— Semantic Merge Conflicts—before a single line of implementation code is synthesized. Simultaneously, we explicitly rule out two common anti-patterns as non-goals: • Human-Editable or Stylistically “Clean” VIR: The VIR is an intermediate synthesis target for agents, not a human programming language, and is never designed to be hand-edited, formatted, or stylistically reviewed by humans. • Trusted Heuristics Inside the Verification Kernel: LLM synthesis agents, proof-search heuristics, and optimization tactics remain 100% untrusted; soundness relies exclusively on a minimal logical proof kernel [4] and a formally verified lowering pass.

2. Core Architecture: Specifications to Verification IR (Pillars 1–3) The first three pillars of the architecture are completely logic-agnostic and apply regardless of whether the underlying proof assistant is Lean [19], Rocq [6], Verus [39], Dafny [41], or MetaPRL [24]. Removing human engineers from the source-code authoring loop triggers a structural inversion across the software stack.

2.1 The Stack Inversion (Pillar 1) Design practices that were essential when humans maintained source files become counterproductive overhead when agents synthesize and verify code directly from specifications.

3

Stack Layer

Human-Centric Engineering

Spec-First Agentic Engineering

Primary Artifact

Implementation source code (.cc, .rs, .go) Complex human-ergonomic languages Unverified compiler passes (LLVM) Heavyweight optimizer and codegen Runtime indirection and interfaces

Modular formal specs and shared ontology Minimal Verification IR (VIR)

Source Language / IR Optimization Layer Compiler Role Modularity Change Review

Line-by-line code diffs and unit tests

Agent-synthesized VIR rewrites Thin verified 1-to-1 lowering (CompCert-style) Spec-only; fused across modules in VIR Boundary specs and CI vacuity/benchmark telemetry

As summarized in the comparison above, traditional human-centric software engineering places implementation files (.cc, .rs, .go), heavy optimizing compilers, and runtime modularity boundaries at the center of the workflow, whereas Spec-First Agentic Engineering elevates modular formal specifications and a shared domain ontology to the primary artifact, delegates cross-module fusion and optimization to agent-generated VIR proofs, and reduces the compiler to a thin CompCert-style lowering layer [42].

2.2 The Zero-Code-Review Change Workflow (Pillar 2) If SWEs are forced to read both the formal specification and the implementation code, formal verification becomes a net tax on engineering velocity. In a Spec-First workflow, correctness is offloaded entirely to the mechanical proof kernel, and implementation code is treated like compilergenerated assembly—an opaque build artifact inspected only when profiling an unmodeled hardware bottleneck. To prevent specification review from becoming a new cognitive bottleneck and to guard against an agent subtly gaming or weakening a specification, every change request is gated by four automated guardrails before a human reviewer opens it: • Boundary-Only Change Views: Internal helper lemmas, loop invariants, and VIR implementation files are collapsed by default so the human SWE inspects only diffs to public module interface specifications and shared domain type definitions. • Zero-Axiom and Spec Well-Formedness Gate: A deterministic linter mechanically verifies that the proof relies on zero unverified axioms or escape hatches (sorry, admit, unsafe, assume), and proves that the specification itself is well-formed (⊢ Spec ∈ U_i) so untyped “junk terms” cannot vacuously satisfy a contract. • Automated Vacuity and Mutation Gates: To ensure the agent has not made a theorem vacuously true [5] via contradictory preconditions, CI requires an automatic witness proof (∃ x. Precond(x) ∧ Postcond(f(x))), while an adversarial mutation runner [18] injects synthetic bugs into the generated VIR and verifies that the formal proof breaks on every mutant. • Differential Litmus Vectors and Telemetry: An independent critic agent generates concrete input/output test vectors directly from the natural-language prompt and proves the specification implies them, alongside automated operational telemetry covering latency, heap allocations, and binary size. 4

2.3 Target Language Evolution: The Verification IR (Pillar 3) When verification is performed at the source level, both the formal semantics of the source language and the correctness of the compiler sit inside the TCB. Mainstream languages (C++, Rust, Go) have massive formal semantics because they optimize for human ergonomics, while production compilers (LLVM, GCC) contain large bodies of unverified heuristic code that regularly suffer from miscompilation bugs [60]. Once humans stop reading or editing source code, three simplifications follow: • Convergence to a Verification IR (VIR): Syntactic sugar becomes a pure liability, so the target language evolves into a minimal VIR with a tiny, total formal semantics (a short specification rather than a standard of well over a thousand pages) where all types, memory effects, and control-flow transitions are 100% explicit. • Moving Optimizations from the Compiler to Agent VIR: Instead of trusting an unverified LLVM pass to unroll loops, inline closures, or fuse passes across modules, the coding agent writes already-unrolled, cache-aligned, specialized code directly in the VIR and proves it satisfies the high-level specification. Because the VIR is already optimized, the underlying compiler shrinks into a thin, formally verified 1-to-1 lowering translator (CompCert [42] or CakeML [36] style) targeting a mechanized ISA semantics such as x86lean [59] (a Lean 4 x86-64 user-level semantics built from public sources and differentially validated against the ACL2 x86isa model, with the rows it cannot carry checked on real processors). • Eliminating Source-Level “Clean Code” Overhead: Traditional rules like DRY [29] and deep interface indirection create severe aliasing and framing headaches for formal verification; in our model, DRY lives strictly in the specification while the agent generates flat, aggressively inlined VIR code.

2.4 Memory Management Without Garbage Collectors or Borrow Checkers Removing human engineers from the source layer also resolves the classic systems programming trilemma of memory management: manual malloc/free (fast but memory-unsafe), tracing garbage collection [30] (safe for humans, but adds a massive runtime to the TCB and can threaten tail-latency bounds), and lexical borrow checking [32] (safe and fast, but forces a conservative static heuristic that rejects some aliasing patterns that are safe). Memory Model

TCB and Cost Impact

Agent VIR Synthesis Impact

Architectural Role

Tracing GC (Go / Java / OCaml) Lexical Borrow Checker (Rust) Linear Capabilities (Perceus / FBIP) Lexical Regions (Arena / Verus)

Poor; large runtime TCB, breaks tail latency Good TCB; rigid expressiveness Zero runtime TCB; exact byte accounting Zero runtime TCB; O(1) bulk free

Easy; no deallocation proofs High friction against heuristics Natural local equational rewrite High leverage; no node lifetimes

Avoid for systems code Replaced by proof capabilities Primary mechanism (most code) Graphs and request scopes (the remainder)

As shown in the table above, human-authored specifications remain purely functional (using value semantics with optional bulk memory bounds in the Cost Spec, such as maxHeap(f) ≤ 4 KB), while the agent manages physical memory in the VIR primarily through Perceus/FBIP linear capabilities [52, 43] (we expect most code: trees, buffers, streaming pipelines) and Arena/Verus-style lexical regions [57, 39] with separation tokens (the remainder: cyclic graphs, request scopes). 5

2.5 Performance Engineering and Implementation Directives To allow human engineers to steer concrete data-structure choices and guarantee high performance without polluting functional specifications, the architecture separates correctness, performance bounds, and implementation guidance into three orthogonal channels. Channel

Human SWE Artifact

Trusted Contract

Enforcement Mechanism

1. Functional Spec

Pure math over abstract types: Map(K, V), lookup(insert(m, k, v), k) =v Asymptotic or concrete bounds: steps(lookup) ≤ 4·log2 (N), heapAlloc = 0 1-line strategy hint: #[realize(Index, via = BTree(B = 16))]

Yes (Hard Gate)

Proof kernel checks extensional equality

Yes (Hard Gate)

Kernel ANF step weights + CI telemetry

No (Untrusted)

Steers agent tactic search and seeding

2. Cost and Resource Spec

3. Implementation Directives

This three-channel separation supports two synergistic workflows: • Non-Binding Implementation Directives and Quotient Realizations: In Extensional CTT, an abstract specification type like Map(K, V) is defined as a Quotient / Partial Equivalence Relation (PER) over concrete realizations [13]. When an SWE attaches a directive such as #[realize(Index, via = BTree(B = 16))] (or fanout = 16), downstream modules and security reviewers still see only the pure mathematical Map(K, V), and swapping the directive to RadixTree breaks zero downstream specifications or caller theorems. • Provable Cost Semantics and Agentic Pareto Search: Because the VIR is in A-Normal Form (Functional SSA) [20, 3], every step and allocation has an explicit cost weight checked against bounds like steps(lookup) ≤ 4·log2 (N) and heapAlloc = 0. Meanwhile, micro-architectural tuning (cache-line alignment, SIMD lane width, prefetching) is handled by the Shared Synthesis Fleet as an autonomous Pareto search problem across candidate realizations benchmarked against production replay traces.

3. Readability and Rewrite Ergonomics: Extensional Logic and HOAS (Pillar 4) Putting the Spec → VIR architecture into practice exposes two critical bottlenecks: Specification Readability for the human reviewer and Rewrite Ergonomics for the synthesis agent. We address these through (1) an Extensional Logical Framework based on Computational Type Theory (CTT— underlying Nuprl [13], MetaPRL [24], and RedPRL [2]) and (2) Higher-Order Abstract Syntax (HOAS) [50, 11] in the VIR. Stated at the strength supported by current evidence, CTT buys the synthesis agent frictionless rewriting (a result measured for a hand-written formal compiler, Section 3.2, which we expect to carry over to synthesis agents), and for the human reader it removes coercions at module boundaries while shifting the well-formedness guarantee from the typechecker to a CI gate (Section 2.2, Gate 2). Whether that tradeoff yields a net improvement in human specification readability is an open empirical question addressed by the experiment in Section 3.3, whose protocol is frozen before the first reader is run. 6

3.1 Extensional CTT vs. Intensional CIC/Lean Intensional dependent type theories with strong normalization—such as the Calculus of Inductive Constructions (CIC) [15, 6] in Lean [19] and Rocq—are the basis of the most widely used provers, and decidable type checking of proof terms is one of their design goals. However, strong normalization and intensional typing require termination arguments for potentially diverging loops or partial parsers, and represent subset constraints as pairs of data and proof that cross module boundaries via explicit coercions. In an agent-driven workflow where humans never read proof scripts, Computational Type Theory (CTT) layers semantic, extensional types [44] over untyped terms without requiring strong normalization [13]. Framework Dimension

Extensional CTT Style

CIC / Lean / Rocq Style

Impact on Readability and Search

Consistency Mechanism

Semantic PERs over untyped terms Extensional and erased { x : A | P(x) } Frictionless untyped lam{x. e}

Syntactic strong normalization Intensional Sigma pairs ⟨x, h_P⟩ Typed binders require Eq.rec / HEq

HOAS Support

Native primitive lam{x. e}

Blocked by strict positivity

Typechecking Decidability

Undecidable; proved via tactics

Decidable automatic kernel check

CTT specifies partial programs directly CTT needs no boundary coercions (↑b, .val) CTT removes transport casts in search (not measured here) Direct meta-level β-reduction in CTT Agents discharge ⊢ Spec ∈ U_i in CI

Subset and Quotient Types Rewriting Under Binders

Two foundational technical considerations govern the use of CTT in this architecture: • Predicativity in CTT: Because CTT’s universe hierarchy is predicative (U1 ⊂ U2 ⊂ U3 ...), quantifying over types or state predicates bumps a specification to the next universe level. However, because CTT terms are untyped and recursive types (µ) plus dependent intersections (x:A ∩ B[x]) [35] are built directly into the PER semantics, implementation code remains universefree, and schematic universe polymorphism infers level offsets invisibly in the background. • The Trusted Core in CTT: While intensional systems like Lean already enjoy small, independently re-implemented proof kernels [9], CTT historically placed its refiner in the trusted base. In our agentic architecture, the refiner, every tactic, and the synthesis agent are all untrusted: a recorded proof certificate (as supported by MetaPRL) is checked against a small core whose rules are verified against the PER semantics, building on Anand and Rahli’s Coq formalization of Nuprl’s semantics (ITP 2014) [1]. A verified certificate checker for the VIR’s logic is a proposed component (Section 7), and Pillar 3’s TCB claim is conditional on it.

3.2 Eliminating Agent Rewrite Friction: HOAS vs. First-Order Binders Because the coding agent performs aggressive source-level optimizations—inlining functions across modules, specializing closures, and fusing loops—every friction point in variable binding and substitution multiplies token consumption and proof-search depth. In empirical formal compiler work (Hickey and Nogin, Formal Compiler Construction in a Logical Framework [25, 23]), representing binders with HOAS in MetaPRL reduced the formal rewrite rules for CPS conversion, closure conversion, and code generation to 484 lines of formal mathematics—compared to 12,000 lines in a traditional compiler—and cut implementation time by 3×.

7

VIR Requirement

HOAS / PHOAS Representation

CompCert First-Order (IDs + Env)

Architectural Verdict

Agent Inlining

Free via meta-level β-reduction Compact local capture-avoiding rewrites Hard in pure HOAS; hides steps

High proof tax; fresh ID maps High friction; environment shifting lemmas Natural explicit state machine

HOAS wins for optimization throughput HOAS wins on token economy First-order wins at machine boundary

Code Motion and Fusion Operational Cost Model

The Hybrid VIR Solution: Three-Stage Lowering Pipeline To combine the algebraic rewrite speed of HOAS with the cycle-accurate operational semantics of CompCert [42] at the hardware boundary, our VIR uses a three-stage lowering pipeline: • Linear Functional SSA with Untyped HOAS Binders: Every intermediate computation in the VIR is explicitly let-bound in A-Normal Form—written in display form as let_lin{x = op(a, b) in e} and desugaring to the canonical MetaPRL operator let_lin{op(a, b); x. e[x]}—which is mathematically isomorphic [3] to Static Single Assignment (SSA) [17] with block arguments [38], making operational execution steps and allocation costs 100% explicit while providing free capture-avoiding substitution [50, 46]. • Linear and Affine Resource Typing: Combining HOAS binders with linear ownership types [21] ensures that a functional binding let_lin{r1 = add(r1, r2) in e} statically guarantees the previous state of r1 is never referenced again, compiling directly to an in-place destructive hardware register or buffer update without continuation-passing overhead. • Register Allocation as Verified α-Conversion: Rather than verifying a complex graphcoloring allocator [10] inside the TCB, an untrusted agent heuristic proposes a physical register assignment that the logical framework validates [51, 54] as a scope-preserving, non-aliasing α-conversion before emitting straight-line machine code via a thin CompCert-style assembler. HOAS-Native Memory Management Pairing CTT with HOAS turns the memory model of Section 2.4 into four local syntactic operations where variable scoping enforces memory safety: • Functional-But-In-Place (FBIP) Reuse via HOAS Rewrites: Pairing linear bindings (let_lin) with Perceus-style reuse rewrites [52, 43] (free(x); let_lin{y = alloc(sz) in e[y]} ↔ let_lin{y = reuse(x) in e[y]}) keeps the specification pure while mutating memory in place with zero heap allocation. • Lexical Regions as HOAS Binders (Free Escape Analysis): The VIR provides a region binder let_region{ρ. e[ρ]} supporting O(1) bump allocation (alloc_in(ρ, sz)); because ρ is a bound meta-variable in HOAS, the standard typing rule requires ρ ∈ / FV(ResultType), automatically guaranteeing [57, 40] that no pointer tied to region ρ can escape and enabling O(1) bulk deallocation on scope exit. • First-Class Permission Tokens for Intrusive Aliasing: For kernel page tables, doublylinked lists, or lock-free ring buffers, CTT separates the copyable integer address (addr : U64) from the linear ownership predicate (perm : Own(addr, T)) [53, 39] threaded through let_lin binders. 8

• Concurrency and Shared-Memory Parallelism via Fractional Permissions: Following Concurrent Separation Logic [49] (Iris [31] / Verus [39] style), an exclusive token Own(addr, T) splits via a verified HOAS rewrite into fractional [8] read-only tokens Read(addr, T, q/2) across concurrent readers and reassembles upon join, while channel sends (send{ch, addr, perm; e}) linearly consume perm in the sender’s scope and transfer it to the receiver.

3.3 A Planned Empirical Evaluation of Specification Readability While the agent-side rewrite gains in Section 3.2 rest on published measurements of a hand-written formal compiler, the human- and model-reader gain has not yet been measured and carries a natural confound: language models and engineers have very likely read far more Lean than CTT. To separate intrinsic readability from familiarity, we define an experiment whose protocol is drafted, and frozen before any reader is evaluated: • Paired Specifications: Five specifications—(1) the router ACL, (2) a wire-format round trip, (3) a token-bucket cost bound, (4) an abstract Map with a quotient realization, and (5) a region-escape property—are each written in their best idiomatic style in both Lean and CTT and verified by an independent third party to state the exact same property. • Familiarity Baseline: A third rendering of each specification is prepared in neutral mathematical notation as a familiarity baseline. • Evaluation Protocol: Comprehension questions are authored from plain-English intent by a non-author, including one trap question per pair that the specification does not answer, alongside a certificate control (a specification with one deliberately wrong clause to catch readers answering from memory rather than the page). • Reader Cohorts: Fresh model readers from two LLM vendors and a human cohort of software engineers unfamiliar with both systems are scored strictly by artifact with raw outputs preserved. • Declared Asymmetry: The Lean specifications are mechanically checked by Lean, whereas the CTT specifications are checked by hand because none of the CTT provers we know of (Nuprl, MetaPRL, RedPRL) has a toolchain we could use for this experiment—an asymmetry that directly informs the well-formedness gate requirement of Section 2.2.

4. Organizational Scaling: Multi-SWE Collaboration (Pillar 5) Treating verification agents as isolated “one-agent-per-human” tools across an organization of hundreds of SWEs would be analogous to asking every developer to run a private compiler and check raw binaries into Git. Instead, organizational scaling relies on a Two-Tier Agent Infrastructure and new collaboration primitives.

4.1 Two-Tier Agent Infrastructure • Tier 1 — Personal Spec-Copilot (1 per SWE): Each engineer interacts with a low-latency Spec-Copilot in their local IDE or change-review interface that helps formalize domain intent into clean CTT specifications, translates formal contracts back into plain-English edge-case summaries, queries upstream and downstream team contracts, and runs instant vacuity checks.

9

• Tier 2 — Shared Synthesis Fleet (Organization Compute Backplane): Operating as continuous shared infrastructure, the Shared Synthesis Fleet consumes the repository’s global graph of approved specifications, synthesizes cross-module HOAS VIR, maintains proofs across repository-wide spec updates, checks cross-team logical consistency, and compiles globally fused machine binaries.

4.2 Collaboration Primitives: Semantic Merges, Ontology, and TCB Debt • Semantic Merge Conflicts Replace Textual Git Conflicts: When Engineer A and Engineer B submit concurrent specification changes (S_A and S_B), the Shared Fleet searches within a compute budget for the vacuity witness required by S_A ∧ S_B (Section 2.2, Gate 3). Because satisfiability is undecidable in general [12], the primitive is the witness rather than a decision procedure: if found, the fleet synthesizes a unified VIR satisfying S_A ∩ S_B; if not found within budget, the fleet halts the merge and issues a Semantic Merge Conflict containing either a concrete counterexample state (when a refutation is found) or the unsatisfied conjunction (when the search exhausts its budget). • Decoupling Conway’s Law [14] from Runtime Performance: Five teams can own five cleanly separated modular specifications while the Shared Synthesis Fleet fuses them via HOAS β-reduction into a single, zero-copy VIR pipeline without microservice or data-copying boundaries. • Ontology Governance and Open-Source “Spec Commons”: Senior and Staff SWEs shift their coordination effort from reviewing code style to governing the Shared Domain Ontology— the minimal set of base types and predicates that allow independent team specs to compose without adapter boilerplate. Open-source communities maintain a shared reference specification and accept zero-trust VIR + Proof Certificate contributions (such as hardware-specific SIMD optimizations) whenever the kernel verifies the proof in milliseconds and benchmarks confirm a Pareto improvement. • Proof-Timeout Escalation and Tracked TCB Debt: When a valid specification exceeds the Shared Synthesis Fleet’s proof compute budget, the fleet follows a two-step escalation protocol rather than asking humans to debug VIR proof scripts: (1) it prompts the SWE via their Personal Copilot to add a 1-line Strategy Directive (Section 2.5) or factor the monolithic spec into two smaller module contracts; (2) for urgent production hotfixes, it isolates the unproven subgoal behind a dynamic Runtime Contract Monitor (assert!) [45], logging the assumption explicitly in the repository’s TCB Debt Ledger until background proof search closes the obligation.

4.3 Brownfield Adoption Regimes Real-world adoption must coexist with massive brownfield C++ and Rust codebases, separating subsystems into two distinct regimes based on coupling and behavioral surface.

10

Brownfield Regime

Architectural Characteristics

Recommended Migration Path

Regime A: Bounded-Surface / High-Risk

Wire parsers, crypto/TPM, ACLs, narrow VMM device models

Regime B: Deeply Coupled Ecosystem

Large stateful C++ object graphs and bidirectional C++/Rust interop

Spec extraction, differential fuzzing against legacy oracle, VIR re-synthesis behind C-ABI shim Stay on host platform (Safe Rust + Crubit [16]) and apply host-language verification (Verus [39])

In Regime A, teams avoid verifying messy legacy C++ in place by using the legacy binary as a behavioral oracle for adversarial differential fuzzing during spec extraction, locking the humanaudited CTT spec, and replacing the legacy implementation behind a C-ABI shim guarded by runtime boundary monitors.

5. Case Study 1 (Technical): Zero-Copy Authenticated Message Router To demonstrate Pillars 1–4 in action, we examine the specification, synthesis, and verification of a Zero-Copy Authenticated Message Router that ingests raw network frames from a ring buffer, parses the wire header and topic identifier, verifies sender permissions against an Access Control List (ACL), enforces a token-bucket rate limit, and forwards authorized payload slices downstream.

5.1 The Engineering Dilemma and Modular Specifications In traditional systems, separating wire parsing, security ACLs, and rate-limiting into clean modules requires intermediate allocations (ParsedFrame) and slice copies across interfaces, whereas handfusing them into a single C/Rust state machine creates an inscrutable tangle of pointer arithmetic where an off-by-one error risks remote code execution. Under the Spec-First Agentic approach, teams establish a 10-line Shared Ontology (WireBuf, Frame, Principal, Topic) and author three independent specifications. Specification

Mathematical Contract (CTT Syntax)

Engineering Guarantee

Spec A (Wire Protocol)

∀ f : Frame. parse(encode(f)) = inl(f) ∀ b : ValidFrame, p : Principal. route(p, b) = Allow(s) ⇒ frame_topic(b) ∈ ACL(p) ∀ b : ValidFrame, p : Principal. (route(p, b) = Allow(s) ⇒ tokens(p) > 0) ∧ heapAlloc = 0 ∧ steps ≤ 32 + 2·len(b)

Round-trip framing and serialization correctness Unauthorized topics are never routed downstream

Spec B (Security ACL)

Spec C (Rate-Limit and Cost)

Token-bucket enforcement, zero heap allocation, O(len(b)) latency

Contrast Exhibit: Idiomatic Lean vs. Extensional CTT Comparing each logic in its best idiomatic style illustrates the boundary distinction analyzed in Section 3.1. Exhibit A.1 — Lean Specification (idiomatic Prop-carrying subtype, total accessors): 11

abbrev WireBuf := ByteArray def readU32 (b : WireBuf) (i : Nat) : UInt32 := . . .

-- total; exact on a ValidFrame

def ValidFrame := { b : WireBuf // 24 ≤ b.size ∧ readU32 b 0 = MAGIC } def frameTopic (b : ValidFrame) : TopicId := readU32 b 8 theorem route_acl_safe (b : ValidFrame) (p : Principal) : IsRouted (route p b) → CanAccess p (frameTopic b)

Exhibit A.2 — CTT Specification (Extensional Subset Types — Zero Clutter): ∀ b : ValidFrame, p : Principal. IsRouted(route(p, b)) ⇒ CanAccess(p, frame_topic(b))

Both statements share the same top-level shape: fuel is absent from the Lean version because route is defined by well-founded recursion at the definition, and the proof witness is erased in Prop. The remaining difference lies at the module boundary: a CTT ValidFrame is a WireBuf, whereas a Lean ValidFrame is a pair whose value crosses boundaries through a coercion (↑b, .val) visible in goals and error messages, while CTT shifts statement well-formedness to CI Gate 2.

5.2 Agent VIR Synthesis and HOAS Loop Fusion Starting from the conjunction Spec A ∩ Spec B ∩ Spec C, a naive compositional implementation executes three sequential passes over the packet buffer: Exhibit B.1 — Unfused Compositional VIR Term: let_lin{ (b1, hdr) = parse_header(b0) in let_lin{ (b2, tok) = check_rate_limit(b1, hdr.sender) in let_lin{ (b3, ok) = verify_acl(b2, hdr.sender, hdr.topic) in emit_payload(b3, hdr.payload_offset) }}}

Directly under the let_lin HOAS binders, the synthesis agent inlines verify_acl and check_rate_limit via meta-level β-reduction and applies the algebraic slice-coalescing rewrite advance(advance(b, i), j) ↔ advance(b, i + j) (subject to i ≥ 0 ∧ j ≥ 0 ∧ i + j ≤ len(b)). Because CTT binders are untyped, rewriting inside let_lin{b2 = ...} folds all separate header and topic bounds checks into a single upfront guard (len(b0) ≥ 24) and eliminates the intermediate hdr structure without requiring dependent HEq transport casts across length-indexed slice types (Slice (n - 4 - k) to Slice (n - (4 + k))).

5.3 The Zero-Code-Review Gate Scorecard When synthesis completes, the 350 lines of bit-twiddling VIR and 1,200 lines of tactic proof scripts are collapsed by default, and the human reviewer inspects only the 15-line specification diff alongside the automated change scorecard (illustrative figures showing gate structure).

12

Automated Gate

Mechanical Check Performed

Status

1. Kernel Proof and Well-Formedness

Verifies ⊢ route_impl ∈ Spec_A ∩ Spec_B ∩ Spec_C with 0 axioms/admits Proves witness ∃ p, b. IsRouted(route(p, b)) Injects 10 synthetic bugs into VIR and confirms proof fails on all 10 Evaluates 5 independent concrete I/O vectors from natural-language prompt Lowered x86-64 profile: 0 heap allocs, 18 cycles/pkt (P99), 1.4 KB binary

PASS (42 ms)

2. Vacuity and Reachability Gate 3. Adversarial Spec Mutation 4. Concrete Litmus Vectors

5. Operational Telemetry

PASS PASS (10/10 killed) PASS (5/5 matched)

PASS

As shown in the scorecard above, every mechanical, vacuity, mutation, litmus, and operational check passes automatically before human review begins.

6. Case Study 2 (Organizational): Multi-Team Collaboration To illustrate Pillar 5 across a live organization, we follow three engineers collaborating on the Message Router—Alice (Wire Protocol Team), Bob (Security Team), and Carol (SRE / Performance Team)—across four scenarios. The scenarios and their figures are illustrative. Scenario

Traditional Software Engineering

Spec-First Agentic Organization

Act I: Cross-Boundary Feature (8-byte CRC64 header)

Breaks auth offsets and zero-copy logic; 3-team migration and 1,500-line review Unit tests mock setup and pass; dead security rule ships to production Separate files (auth.rs, limits.rs) merge cleanly in Git; OOM crash in prod Maintainers hesitate to merge 2,000 lines of intrinsics due to backdoor risk

Alice edits 12 lines in Spec A; Bob’s ValidFrame spec needs 0 edits; fleet re-fuses VIR Bob’s Copilot Vacuity Gate fails ∃ b. QuarantinePrecond(b) in 3 seconds Fleet finds refutation ⊢ False when rate > 10M ∧ drop(b) and blocks merge Kernel verifies certificate in 40 ms; CI confirms 3.2× gain; merges with 0 code review

Act II: Flawed Spec (Contradictory quarantine rule) Act III: Semantic Merge Conflict (64B log vs. 0B DDoS cap) Act IV: Zero-Trust Open-Source AVX-512 SIMD PR

Across all four acts, human attention remains bounded to domain-level intent and cross-team ontology contracts while the Shared Synthesis Fleet absorbs cross-module fusion, proof maintenance, and regression verification.

7. Risks, Roadmap, Related Work, and Implementation Status 7.1 Risks, Limitations, and Mitigations Shifting human oversight from implementation code to formal specifications introduces three primary failure modes governed by architectural and organizational controls:

13

• Specification Gaming (“Reward Hacking”) [High Severity]: An agent might subtly weaken a specification precondition to make a difficult proof succeed; this is mitigated by locking specification files as read-only during VIR synthesis and enforcing automated Vacuity Proofs and Adversarial Spec Mutation Testing in CI before human review. • Unmodeled Boundary Semantics (FFI / Hardware) [Medium Severity]: Bugs in raw OS syscalls, DMA controllers, or hardware errata outside the formal model are mitigated by isolating raw I/O inside a tiny, human-audited Hardware Abstraction Layer (HAL) paired with runtime contract monitors in production. • Ontology Fragmentation [Medium Severity]: Incompatible base types across teams requiring brittle adapter proofs are prevented by elevating Ontology Architecture to a primary Staff/Principal SWE responsibility.

7.2 Phased Adoption Roadmap Organizations can adopt this architecture incrementally across three phases without a flag-day rewrite: • Phase 1 — Spec-First Review and Differential Oracles on Host Languages (Immediate): Deploy Personal Spec-Copilots and automated vacuity/mutation gates over existing C++ and Rust workflows (e.g., Verus on Rust components and differential fuzzing on bounded C++ subsystems) while tracking Verified Coverage. • Phase 2 — CTT + HOAS VIR Pilot on High-Assurance Bounded Subsystems (Near-Term): Target isolated Regime A components (wire parsers, crypto/TPM routines, ACL evaluators, narrow VMM device models) for full Spec-Extraction and HOAS VIR synthesis behind verified C-ABI shims. • Phase 3 — Shared Synthesis Fleet and Cross-Module Fusion at Scale (Long-Term): Connect modular team specifications into a repository-wide Spec Graph governed by a Shared Domain Ontology to detect Semantic Merge Conflicts and fuse adjacent VIR modules across team boundaries.

7.3 Related Work This architecture sits at the intersection of six research lineages and differs from each in a specific dimension: • Verification-Aware Languages: Dafny [41], F* [56], and Verus [39] place specifications beside human-written code, and Aeneas [27] translates Rust into Lean for proof; Pillar 1 removes the human as implementation author, and Pillar 3 removes the human-ergonomic source language. • Verified Compilers: CompCert [42] and CakeML [36] verify optimizing compiler passes inside the TCB; Pillar 3 moves optimizations above the compiler into agent-verified VIR rewrites, retaining only a thin verified lowering layer. • Computational Type Theory: Nuprl [13], MetaPRL [24], and RedPRL [2] establish the extensional lineage, with Anand and Rahli’s Coq formalization of Nuprl’s semantics providing the verified core precedent and Hickey and Nogin’s MetaPRL compiler providing the HOAS empirical baseline; our work adapts this foundation to autonomous agent synthesis. 14

• Agents Under a Machine Referee: Kaashoek and Zeldovich [33] report a Rocq-checked proof of the xv6 kernel on Sail RISC-V semantics under human-designed intermediate specs, AlphaProof [28] proves competition mathematics in Lean, and SaltBench (arXiv:2609.11076) [26] measures how an external referee alters agent behavior and supplies the cost bounds cited in Section 1.2; our paper defines the organizational engineering layer these results enable. • Formal Methods in Industry: TLA+ at Amazon [47], seL4 [34], IronFleet [22], and Project Everest [7] demonstrate specialist-built verified systems; Pillar 5 examines when agents serve as the verification specialists and generalist SWEs write only specifications. • Memory and Ownership: Perceus reuse [52, 43], Tofte and Talpin’s regions [57], Iris [31], and fractional permissions [8, 49] provide the mechanisms assembled in Sections 2.4 and 3.2 under HOAS binders in an agent-synthesized IR.

7.4 Separation of Existing Baselines and Proposed Components This paper is a proposal. To allow readers to weigh each architectural pillar by its current empirical grounding, the table below separates built and measured systems from proposed components. Component

Status

Evidence Base

Spec-first review gates (lint, vacuity, mutation, non-author reads) Agent evaluation under a machine referee (200-condition pilot) Mechanized x86-64 user-level ISA semantics HOAS formal compiler construction in CTT Verification IR (linear functional SSA, regions, permissions) Thin verified lowering and register allocation via α-conversion Verified certificate checker for VIR logic Two-tier fleet, semantic merge conflicts, TCB debt ledger Spec-readability experiment and review-surface ratio

Built and in daily use

Public salt (Lean 4) repository CI [55]

Built and published

SaltBench (arXiv:2609.11076)

Built and validated Prototyped in MetaPRL (toolchain not current) Proposed

Public x86lean (Lean 4) repository [59] Hickey and Nogin (484 vs. 12,000 lines) Defined in this paper

Proposed

Targets x86lean semantics

Proposed

Precedent in Anand and Rahli (ITP 2014) Defined in this paper

Proposed Commissioned / protocol frozen before the first reader

Forthcoming empirical study

Pillars 1 and 2 rest on the first two rows (salt and SaltBench), Pillar 3 on the third (x86lean), Pillar 4 on the fourth (Hickey and Nogin) and the planned readability experiment, and Pillar 5 is an architectural argument.

Appendix: Formal CTT Specifications and HOAS VIR Rewrite Rules This appendix presents the concrete mathematical definitions and bidirectional term-rewriting rules underpinning Case Study 1 (Section 5), following the HOAS and second-order substitution conventions of Computational Type Theory (Hickey and Nogin) where syntax nodes take the 15

canonical form opname[params]{v1 . t1 ; ...; vm . tm } and second-order metavariable e[v] performs automatic capture-avoiding substitution e[t].

A.1 Shared Domain Ontology and Extensional Subset Types (CTT) Because subset membership proofs in CTT { x : A | P(x) } are semantic judgments over PERs rather than syntactic pair components, runtime VIR terms carry zero proof-term overhead: (* Base Types and Wire Layout Constants *) Byte ≡ { i : Int | 0 ≤ i < 256 } U32 ≡ { i : Int | 0 ≤ i < 2 32 } WireBuf ≡ Array(Byte) Principal ≡ U32 TopicId ≡ U32 MAGIC ≡ 0x4D534731 (* "MSG1" wire header magic *) (* Extensional Subset Type for Valid Network Frames *) ValidFrame ≡ { b : WireBuf | len(b) ≥ 24 ∧ read_u32(b, 0) = MAGIC } (* Semantic Projections over ValidFrame (No Bounds Witnesses Required) *) frame_sender(b) ≡ read_u32(b, 4) frame_topic(b) ≡ read_u32(b, 8) frame_pay_off(b) ≡ read_u32(b, 12) frame_pay_len(b) ≡ read_u32(b, 16)

A.2 Linear Functional SSA VIR Grammar and Foundational Rewrite Rules The VIR is an A-Normal Form (Functional SSA) language where every intermediate operation is bound by an untyped HOAS binder and let_lin enforces single-use linear ownership: (* Atoms a and Linear Functional SSA Expressions e *) a ::= i | true | false | v | a 1 binop a 2 | a 1 relop a 2 e ::= let_atom{a; v. e[v]} | let_lin{op(a 1 , ..., an ); b. e[b]} | advance{b; offset; s. e[s]} | read_u32{b; offset; v. e[v]} | guard{a_cond; e_ok; e_err} | return{a} | drop{code}

(* Pure atom binding *) (* Linear buffer/state binding *) (* Zero-copy slice advance *) (* Bounded 32-bit wire read *) (* Branching bounds/ACL guard *) (* Terminal outcomes *)

Capture-avoiding inlining, dead-code elimination, constant folding, and branch pruning require four bidirectional equivalence rules (redex ↔ contractum).

16

Rule Name

Bidirectional HOAS Rewrite Rule

Side-Condition and Role

[beta_lin]

let_lin{v1 ; v2 . e[v2 ]} ↔ e[v1 ]

[dce_atom]

let_atom{a; v. e[]} ↔ e[]

[const_fold]

(i binop j) ↔ [[binop]](i, j)

[guard_true]

guard{true; e1 ; e2 } ↔ e1

Meta-level capture-avoiding substitution for cross-module inlining Second-order pattern e[] ensures v ∈ / FV(e) for non-trapping a Evaluates constant 32/64-bit arithmetic and guards at synthesis time Prunes unreachable error branches once composite guard holds

A.3 Step-by-Step Derivation: Fusing the Message Router Pipeline To fuse Wire Header Parsing (Spec A), Token-Bucket Rate Limiting (Spec C), and Security ACL Verification (Spec B) into a single zero-copy pass, the agent applies three domain-specific algebraic rewrites over buffer slices: (* Rule 1: Slice-Advance Coalescing *) [slice_fuse] advance{b; i; s 1 . advance{s 1 ; j; s 2 . e[s 2 ]}} ↔ advance{b; i + j; s 2 . e[s 2 ]} (when i ≥ 0 ∧ j ≥ 0 ∧ i + j ≤ len(b)) (* Rule 2: Guard Hoisting & Conjunction Merging *) [guard_merge] guard{c 1 ; guard{c 2 ; e_ok; e_err}; e_err} ↔ guard{c 1 ∧ c 2 ; e_ok; e_err} (* Rule 3: Offset Read Commutation Across Disjoint State *) [read_comm] read_u32{b; i; v 1 . let_lin{upd_bucket(st, v 1 ); st'. read_u32{b; j; v 2 . e[v 1 ; st'; ,→ v 2 ]}}} ↔ read_u32{b; i; v 1 . read_u32{b; j; v 2 . let_lin{upd_bucket(st, v 1 ); st'. e[v 1 ; st'; ,→ v 2 ]}}}

Applying [beta_lin], [guard_merge], [slice_fuse], and [dce_atom] in sequence yields the fused single-pass, zero-allocation VIR term: (* Synthesized & Fused Single-Pass VIR Term *) guard{ len(b 0 ) ≥ 24; read_u32{ b 0 ; 0; magic. read_u32{ b 0 ; 4; sender. read_u32{ b 0 ; 8; topic. guard{ magic = MAGIC ∧ can_access(sender, topic) ∧ has_tokens(bucket_st, sender); let_lin{ dec_tokens(bucket_st, sender); bucket_st'. advance{ b 0 ; 24; payload_slice. return{ (bucket_st', payload_slice) } } }; drop{ ERR_UNAUTHORIZED_OR_RATE_LIMITED } } } } }; drop{ ERR_TRUNCATED_FRAME } }

A.4 Lowering to Scoped Assembly and Register Allocation via α-Conversion Following Section 4 of Hickey and Nogin, the target instruction set is formalized using scoped immutable register bindings where instructions modifying a destination register bind a fresh metavariable for the continuation (ADD o1 , %v2 , λv3 . e[v3 ]), memory writes use non-binding forms (MOV %v1 , offset(%v2 ); e), and register pressure spills use scoped spill instructions (SPILL %v1 , λs. 17

e[spill[v1 , s]]). An untrusted Chaitin-style graph-coloring heuristic proposes a mapping from VIR variables (b0 , magic, sender, topic, payload_slice) to physical x86-64 registers (%rdi, %eax, %ecx, %edx, %rsi), which the proof kernel verifies purely as a capture-avoiding α-conversion: (* Exhibit A.4: Lowered Scoped x86-64 Assembly for the Fused Router Fast-Path *) (* Input: %rdi = b 0 base ptr, %rsi = b 0 byte len, %rdx = bucket_st ptr *) CMP $24, %rsi JB then drop_truncated else (* unsigned: the length is a byte count *) MOV 0(%rdi), λ%eax. (* magic ← b 0 [0..3] *) CMP $0x4D534731, %eax JNE then drop_unauthorized else MOV 4(%rdi), λ%ecx. (* sender ← b 0 [4..7] *) MOV 8(%rdi), λ%r8d. (* topic ← b 0 [8..11] *) LEA ACL_BITMAP(%rip), λ%r9. (* RIP-relative takes no index *) BT %r8, 0(%r9, %rcx, 8) (* constant-time ACL bit test *) JNC then drop_unauthorized else CMP $0, BUCKET_ARR(%rdx, %rcx, 4) (* the bucket is tested before it is written *) JLE then drop_rate_limited else SUB $1, BUCKET_ARR(%rdx, %rcx, 4) (* in-place linear token update *) LEA 24(%rdi), λ%rax. (* payload_slice ← b 0 + 24 *) SUB $24, %rsi (* payload length = len - 24 *) JMP emit_slice (* on entry: %rax = payload, %rsi = its length *)

At lowering time, the functional linear state token bucket_st erases into the exclusive base-pointer capability %rdx, so that let_lin{dec_tokens(bucket_st, sender); bucket_st’. ...} lowers to the in-place memory instruction SUB $1, BUCKET_ARR(%rdx, %rcx, 4), placed after the bucket is tested, with the processor condition flags (JB, JNE, JNC, JLE) modeled as scoped branching continuations. What is checked. Exhibit A.4 is the lowering as repaired. Its machine code, assembled by a standard assembler, is checked in the x86lean semantics [59] against the router’s functional specification: for every start state whose registers and memory encode the specification’s inputs (the buffer, the ACL table and the bucket state), in which topic < 64 and the buffer does not overlap the sender’s bucket cell (the one cell written), the program stops at an exit for the specification’s outcome (the combined unauthorized-or-rate-limited outcome may take either of its two labels), with memory unchanged on each drop, and on emit_slice with %rax = b0 + 24, %rsi = len − 24 and exactly one bucket cell decremented (theorem repaired_refines in Router/Refines.lean at x86lean commit adbf22f995d2 [48]). A first draft of this exhibit was not a refinement, and two concrete states refute it: it compared the length as a signed number (a length of 263 or more was dropped as truncated), and it decremented the bucket before testing it (a bucket of 0 became 0xFFFFFFFF on a drop). It also used a RIP-relative address with an index register, which cannot be encoded, and its exit passed no slice length. The listing above repairs those four. The fifth, topic < 64, is a precondition of the theorem rather than a repair, since the 32-bit TopicId of A.1 does not supply it. Not claimed: the α-conversion check and the register allocator described above are not built; the theorem is about these instructions, not about a procedure that produces them; and it relates one run of the program to one application of the specification. A second theorem covers two successive calls with the bucket state threaded through: the second call refines the specification applied to the state the first call returned, so two emits from one sender need at least two tokens at the start and leave that sender’s bucket cell two lower (two_calls in Router/MultiCall.lean at the same commit [48], and two_emits_same_sender in compose/Compose/RateLimit.lean at vir commit 7595dfd8d128 [58]). Its limits: it is about two calls, not n; between them the caller writes only the second call’s buffer; and since the lowering does not bound the sender, that buffer must miss a 235 -byte ACL table and a 234 -byte bucket array, and the two tables must not overlap, which

18

requires about 48 GiB of address space for the tables. That last limit is a property of the object as written, not of the proof. The theorem holds in the x86lean model at a pinned public revision; this program has not been run on hardware, and the model’s differential validation covers instruction forms, not this program. Code is not in memory in the model, so self-modifying code is outside what is checked.

References [1] Abhishek Anand and Vincent Rahli. Towards a formally verified proof assistant. In Interactive Theorem Proving (ITP 2014), Lecture Notes in Computer Science, pages 27–44. Springer, 2014. [2] Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, and Jonathan Sterling. The RedPRL proof assistant (invited paper). In Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), volume 274 of Electronic Proceedings in Theoretical Computer Science, pages 1–10, 2018. [3] Andrew W. Appel. SSA is functional programming. ACM SIGPLAN Notices, 33(4):17–20, 1998. [4] Henk Barendregt and Freek Wiedijk. The challenge of computer mathematics. Philosophical Transactions of the Royal Society A, 363(1835):2351–2375, 2005. [5] Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh. Efficient detection of vacuity in temporal model checking. Formal Methods in System Design, 18(2):141–163, 2001. [6] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science, an EATCS Series. Springer, 2004. [7] Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017), volume 71 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1–1:12. Schloss Dagstuhl – LeibnizZentrum für Informatik, 2017. [8] John Boyland. Checking interference with fractional permissions. In Static Analysis (SAS 2003), Lecture Notes in Computer Science, pages 55–72. Springer, 2003. [9] Mario Carneiro. Lean4Lean: Verifying a typechecker for Lean, in Lean. arXiv:2403.14064, 2024. [10] G. J. Chaitin. Register allocation & spilling via graph coloring. In Proceedings of the 1982 SIGPLAN Symposium on Compiler Construction, pages 98–101. ACM, 1982. [11] Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08), pages 143–156. ACM, 2008. [12] Alonzo Church. A note on the Entscheidungsproblem. Journal of Symbolic Logic, 1(1):40–41, 1936. 19

[13] R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, NJ, 1986. [14] Melvin E. Conway. How do committees invent? Datamation, April 1968. [15] Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2–3):95–120, 1988. [16] Google. Crubit: a bidirectional bindings generator for C++ and Rust. https://github.com/ google/crubit, 2022–. [17] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 13(4):451–490, 1991. [18] R.a. DeMillo, R.j. Lipton, and F.g. Sayward. Hints on test data selection: Help for the practicing programmer. Computer, 11(4):34–41, 1978. [19] Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction (CADE-28), Lecture Notes in Computer Science, pages 625–635. Springer, 2021. [20] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI ’93), pages 237–247. ACM, 1993. [21] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1–101, 1987. [22] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet: Proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15), pages 1–17. ACM, 2015. [23] Jason Hickey, Aleksey Nogin, Adam Granicz, and Brian Aydemir. Formal compiler implementation in a logical framework. Caltech Computer Science Technical Report CaltechCSTR:2003.002, California Institute of Technology, April 2003. [24] Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL – a modular logical environment. In Theorem Proving in Higher Order Logics (TPHOLs 2003), Lecture Notes in Computer Science, pages 287–303. Springer, 2003. [25] Jason Hickey and Aleksey Nogin. Formal compiler construction in a logical framework. HigherOrder and Symbolic Computation, 19(2-3):197–230, September 2006. [26] Jason Hickey. SaltBench: A referee-gated protocol for measuring method effects in machinechecked software work, 2026. Version 3, 2 October 2026. [27] Son Ho and Jonathan Protzenko. Aeneas: Rust verification by functional translation. Proceedings of the ACM on Programming Languages, 6(ICFP):711–741, 2022. 20

[28] Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salvatore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Velingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli, and David Silver. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651(8106):607–613, 2026. Published online 12 November 2025. [29] Andy Hunt and Dave Thomas. The Pragmatic Programmer. Addison-Wesley, 1999. [30] Richard Jones, Antony Hosking, and Eliot Moss. The Garbage Collection Handbook: The Art of Automatic Memory Management. Chapman and Hall/CRC, second edition, 2023. [31] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. [32] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL):1–34, 2018. [33] M. Frans Kaashoek and Nickolai Zeldovich. Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents, 2026. arXiv:2609.04043v3, 12 October 2026. [34] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP ’09), pages 207–220. ACM, 2009. [35] A. Kopylov. Dependent intersection: A new way of defining records in type theory. In 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pages 86–95. IEEE, 2003. [36] Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14), pages 179–191. ACM, 2014. [37] C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization (CGO 2004), pages 75–86. IEEE, 2004. [38] Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. MLIR: Scaling compiler infrastructure for domain specific computation. In 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pages 2–14. IEEE, 2021. [39] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315, 2023. 21

[40] John Launchbury and Simon L. Peyton Jones. Lazy functional state threads. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI), pages 24–35. ACM, 1994. [41] K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Lecture Notes in Computer Science, pages 348–370. Springer, 2010. [42] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. [43] Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP2 : Fully in-place functional programming. Proceedings of the ACM on Programming Languages, 7(ICFP):275–304, 2023. [44] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. [45] B. Meyer. Applying “design by contract”. Computer, 25(10):40–51, 1992. [46] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991. [47] Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon web services uses formal methods. Communications of the ACM, 58(4):66–73, 2015. [48] Jason Hickey. The O95 router spike. Branch spike/o95-router of https://github.com/jyh/ x86lean; the theorems cited are at commit adbf22f995d2, 2026. [49] Peter W. O’Hearn. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1-3):271–307, 2007. [50] F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI ’88), pages 199–208. ACM, 1988. [51] A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1998), Lecture Notes in Computer Science, pages 151–166. Springer, 1998. [52] Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. Perceus: Garbage free reference counting with reuse. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21), pages 96–111. ACM, 2021. [53] J.c. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pages 55–74. IEEE, 2002. [54] Silvain Rideau and Xavier Leroy. Validating register allocation and spilling. In Compiler Construction (CC 2010), Lecture Notes in Computer Science, pages 224–243. Springer, 2010. [55] Jason Hickey. salt. Software, Apache-2.0, 2026.

22

[56] Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16), pages 256–270. ACM, 2016. [57] Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997. [58] Jason Hickey. vir: a Verification IR measured in two logics (Lean 4 and MetaPRL). Software, release v0.1.0, commit 7595dfd8d128, 2026. https://github.com/jyh/vir. doi:10.5281/zenodo.23870938. [59] Jason Hickey. x86lean: An x86-64 user-level ISA semantics in Lean 4, differentially validated against public models. Software, Apache-2.0, 2026. [60] Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 283–294. ACM, 2011.

23

Related documents

• Towards Agentic Proof Harness Engineering#1387525
• Towards Agentic Proof Harness Engineering#1375108
• Agent4Spec: An LLM-based Agentic System to Optimize API Specifications through Automated Validation and Market Analysis#1297625
• Agent4Spec: An LLM-based Agentic System to Optimize API Specifications through Automated Validation and Market Analysis#1291872
• Methodological Harness in Agentic Software Engineering: An Empirical Study on Mining Software Repositories#1115970