Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale
Jason Hickey
cs.SE
Nov 1, 2026 · v1
cs.LO
TL;DR
Builds on the authors' Lean 4 artifacts (salt review gates, x86lean ISA semantics, vir IR) and contrasts idiomatic Lean specifications with extensional CTT.
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 agent-authored, 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.
Problem
When coding agents generate implementation code, formal specifications, and proofs together, human review of code becomes the bottleneck. A software engineering architecture is needed in which humans review only formal specifications.
Approach
The paper proposes a logic-agnostic spec-first stack inversion. In this stack, CI gates (kernel proof, vacuity, mutation testing, litmus vectors, telemetry) replace code review. A minimal Verification IR is lowered by a thin verified translator. It argues for an extensional Computational Type Theory specification layer with HOAS and linear resource typing, and contrasts idiomatic Lean subtypes with CTT subset types. It also outlines two-tier agent infrastructure for multi-team organizations. Existing baselines include the Lean 4 repositories salt and x86lean, a vir IR measured in Lean 4 and MetaPRL, and SaltBench.
Results
The architecture is illustrated on a zero-copy authenticated message router. The reported gates passed: a 42 ms kernel check, 10/10 synthetic bugs killed, and 18 cycles per packet. The organizational case study is illustrative. A readability experiment is defined with its protocol frozen before the first reader, and several components remain proposals rather than implementations.
| Gate | Check | Status |
|---|
| Kernel proof | route_impl meets Spec A∩B∩C, 0 axioms/admits | PASS (42 ms) |
| Vacuity | witness ∃p,b. IsRouted(route(p,b)) | PASS |
| Spec mutation | 10 injected bugs | PASS (10/10 killed) |
| Litmus vectors | 5 concrete I/O vectors | PASS (5/5) |
| Telemetry | 0 heap allocs, 18 cycles/pkt, 1.4 KB | PASS |
Automated CI gates for the message router case study
