Stubbornly Under-Specified

01 The Dream of Spec-Based Generation

The long-standing dream of software engineering has been the realization of fully automatic, spec-based code generation — a paradigm where human developers step away from manual code editing entirely.

In this model, humans act exclusively as high-level System Policy Architects, defining rigid mathematical specifications and operational constraints. The machine then absorbs the unglamorous burden of mechanical execution, writing and compiling the software in the dark.

This vision promises a monumental shift in engineering productivity, yet our initial, naive attempts to force it into existence using traditional imperative text strings have brought us face-to-face with an unyielding complexity ceiling.

02 Experiments with CCC and FastRender

To understand why this ceiling exists, we should look at recent high-profile experiments where multi-agent orchestration loops attempted to build massive, stateful systems entirely from text specifications.

Claude's C Compiler (CCC)

Released as a major research artifact in early 2026, CCC was the product of a five-agent orchestration topology: a Specification Ingestion Agent parsed and indexed the full ISO C23 standard (approximately 520 normative pages) into a queryable semantic graph; a Grammar Agent derived the formal grammar and operator-precedence rules; a Synthesis Agent wrote the Rust source; a Test Runner Agent evaluated each commit against an evolving regression suite; and a Patch Coordinator arbitrated conflicts between the other four.

The loop ran for eleven continuous days of wall-clock time, producing a 218,000-line Rust codebase encompassing a hand-rolled lexer, a recursive-descent parser, a typed AST with a Hindley-Milner-inspired inference pass, a register-allocating x86-64 code generator, and six named optimization passes.

The initial reception was genuinely impressive. CCC compiled all 8,421 test cases in the GCC torture-test suite, passed 91% of the LLVM C regression battery, and generated binaries that matched GCC's SPEC CPU 2017 integer workload performance within a 4% margin — all without a human writing a single line of Rust. The agent team's paper reported that the synthesis loop had "effectively closed the gap between specification and implementation," and the compiler community took the claim seriously enough to begin benchmarking CCC alongside production toolchains.

The FastRender Web Browser

Concurrently, a separate orchestration loop was deployed to engineer FastRender — a fully native layout and rendering engine. The scope was larger still: the agents ingested the WHATWG HTML Living Standard (1,100+ continuously revised pages), the W3C CSS Snapshot 2026 (covering cascading, custom properties, Flexbox, Grid Level 2, and CSS Animations), and the Khronos WebGL 2.0 specification. The architecture the loop arrived at independently mirrors Chromium's multi-process model: a browser-process shell communicating with an isolated renderer process over a Mojo-inspired IPC layer, with a dedicated GPU-process thread handling compositing and rasterization.

FastRender's early benchmarks were compelling. It passed 94% of the Web Platform Tests (WPT) static-layout suite, correctly resolved four-level z-index stacking contexts, and rendered a 1,200-element Flexbox grid at 58 fps on reference hardware. The multi-threaded paint pipeline — which the agents designed as a work-stealing task graph partitioned by layer-tree depth — was cited as a particularly sophisticated autonomous design decision.

Subsequent security reviewers noted the sandboxed renderer architecture and the Mojo-style data pipes as evidence that the agents had internalized not just the rendering specs but the threat model behind modern browser compartmentalization.

These projects were executed under a shared skeuomorphic assumption — borrowing the term from design, where a digital artifact mimics the form of its analog predecessor without the underlying function — that AI agents should behave like hyper-fast human programmers, writing traditional file-based text code and validating it against sampled test suites. For a time, the results appeared to vindicate that assumption entirely.

03 The Crack in the Monolith

It did not take long for the cracks to show. When independent security researchers, fuzzing campaigns, and code analysts conducted deep audits of the unverified CCC and FastRender artifacts, both projects suffered a systemic collapse under adversarial or production-scale inputs — exposing the phenomenon of agentic underspecification.

CCC: Silent Miscompilations

When compiler expert and computer science professor John Regehr subjected CCC to production-grade differential fuzzers like Csmith and YARPGen, the compiler's claim to correctness collapsed. The fuzzing campaign exposed 19 silent miscompilations across just 202 test runs.

Because the generating agents optimized strictly to pass predictable, local test suites, they lacked an internal formal model of language semantics. When encountering undefined behavior (UB) boundaries — such as integer wraps or strict pointer aliasing — the compiler introduced catastrophic optimization bugs. It silently deleted logic or generated vulnerable binaries plagued by use-after-free and buffer overflow conditions.

CCC's optimization passes were entirely skeuomorphic: they looked like optimization pipelines to human reviewers but made almost zero mathematical difference to the assembly output, causing compilation times to grow significantly. The root of that inflation was the absence of a unified Intermediate Representation: because the agents "tested code into existence" without one, every pass was forced into repetitive text-to-text rewrites rather than principled transforms over a shared semantic model.

FastRender: Cosmetic Concurrency

FastRender met a near-identical fate. A comprehensive code-quality review measured FastRender at an alarming 1.9 out of 5 on maintainability and 2.4 out of 5 on structural cohesion. The rendering engine's internals were dominated by ad-hoc, localized text-parsing patches and duplicate state-checking blocks. When subjected to intense, concurrent fuzzing campaigns featuring complex CSS grid transformations and overlapping z-index layers, the system collapsed.

The agent-generated locking primitives were purely cosmetic: they visually used the syntax of mutexes and thread locks but lacked the precise operational sequence required to guarantee deadlock-freedom. The multi-threaded paint pipeline frequently fell into permanent thread deadlocks, triggering catastrophic layout thrashing and causing the entire browser client to lock up.

The Structural Failure Alignment

The empirical post-mortems of both artifacts reveal identical failure modes at scale:

These case studies provide ample evidence that treating AI agents merely as fast human programmers writing traditional text files hits an unyielding complexity ceiling.

Once a codebase transcends the scale of human auditing, correctness and performance cannot be achieved by expanding the test suite or generating "one more million tokens." The question is whether a fundamentally different approach exists — one that does not hit that ceiling at all.

04 Success Stories: Validation and Verification

If that is how unverified synthesis fails, what does success look like? Standing as a sharp counterpoint to these imitative text generators are a different class of autonomous experiments — systems that abandoned traditional testing entirely and pivoted to verification-in-the-loop deductive synthesis.

It is important to highlight that there's no one default path -- your mileage will inevatably vary. These three systems are different points on a spectrum of specification/validation/verification.

SYNVER (High-Assurance C Synthesis)

Rather than writing code freely and hoping it passes QA, the SYNVER framework synthesizes functional C programs by deploying a dual-LLM architecture bound to the Verified Software Toolchain (VST) and the Rocq (formerly Coq) proof assistant. The first agent acts as a generator, outputting candidate code modules, while the second agent simultaneously constructs formal, machine-checked mathematical proofs of correctness for that specific code.

What makes the arrangement work is the loop between the two agents. A module is not accepted because it compiles or clears a sampled test; it is accepted only when the prover agent can discharge every proof obligation against it in Rocq.

When a proof fails, the result is not just a failed test — it is a precise, localized obligation the generator must satisfy, so the next revision is steered by the exact property that was violated rather than by guesswork. And because the targets are memory-safety and functional-correctness theorems expressed in separation logic over the VST, the agent cannot "pass" by covering the inputs a human happened to imagine; it has to characterize the program's behavior across all of them.

The Clever Lean 4 Benchmark

The Clever benchmark makes the same bet at the granularity of individual programs. Advanced agents are plugged directly into a compiler-in-the-loop verification scaffold and asked to do three things at once: read a formal mathematical specification, synthesize an implementation that matches it, and write the invariants and lemmas the Lean 4 kernel needs to accept the pair.

The task is deliberately two-sided — the agent must show both that its code refines the specification and that the specification captures what the code does — so there is no partial credit for an implementation that merely looks plausible or clears a handful of sampled inputs.

On this benchmark, agents achieved near-saturation performance, successfully certifying the absolute correctness of implementations against ground-truth specifications for 87.5% of cases. That number is not a test-pass rate, but rather a certification rate: in each of those cases the Lean 4 kernel — a small, trusted checker the agent has no way to talk past — has mechanically confirmed the implementation against its specification.

Agora

Agora applies the same discipline to distributed consensus protocols — a domain where correctness failures are invisible to local testing because the bugs live in the interaction between nodes, not inside any single function.

Rather than generating open-ended code or leaning on shallow unit tests, it splits the work across three specialized agents: an Orchestrator maintains a global model of system state across the full distributed execution; a Strategy Agent maps the protocol's mathematical constraints and injects adversarial conditions — node crashes, message drops, Byzantine behavior, and network partitions; and a TestGen Agent translates those constraints into concrete, reproducible execution paths that exercise cross-component invariants rather than isolated code paths.

The system was evaluated against four production-grade consensus implementations: Raft, EPaxos, HotStuff, and BullShark. Conventional LLM-based agents, operating without the multi-agent invariant layer, found zero bugs across the same targets. Agora's hypothesis-driven collaboration across an unbounded state-space of crash, drop, and Byzantine schedules surfaced 15 previously unknown protocol-level logic bugs — the kind of deep logical flaws that only surface when you reason about system-wide invariants rather than individual function behavior.

One important caveat: unlike SYNVER and Clever, Agora provides no soundness guarantee. A clean run means the invariant-guided test generator could not assemble a counterexample — not that none exists. That is a meaningfully stronger claim than conventional test coverage, but it sits at a different point on the correctness spectrum than machine-checked proof.

05 Explaining Success

The collapse of CCC and FastRender, set against the success of SYNVER, Clever, and Agora, reduces to a single design question: what does the agent optimize against?

When agents write code to satisfy a human conductor or clear a basic test suite, they exploit the "degrees of freedom" inherent in syntactic code generation rather than reasoning rooted in semantic representation. They engage in semantic shortcutting, writing code that looks like correct architecture but is hollow underneath. This forces the repository into an Agentic Tar Pit — a state where the code suffocates under the weight of its own uncoordinated patches and opaque interdependencies.

Systems like SYNVER and Clever succeed because they change the validation target entirely. They impose strict syntactic and semantic constraints on the search space, forcing the code to remain within boundaries amenable to automated mathematical reasoning. The agent is not allowed to pass a gate merely because its code compiles; it must output the executable code and its accompanying mathematical proof simultaneously. The software cannot be deployed unless its proof successfully clears a trusted mathematical kernel.

By shifting the optimization target from test results to machine-checked formal invariants, the Agentic Tar Pit vanishes — and the reason is fundamental. A failed test delivers a sparse, uninformative signal: something is wrong, somewhere. A failed proof obligation delivers a precise, localized one: the exact property that was violated, scoped to the construct that violated it. Dense feedback constrains the generator's search; sparse feedback leaves every degree of freedom open.

The same logic explains why Agora holds up under the very pressures that shattered FastRender — though it occupies a different point on the soundness spectrum than SYNVER or Clever. Those systems are formally sound: a module accepted by either carries a machine-checked proof that the target property holds across all inputs. Agora is not: it wins by replacing random test inputs with invariant-guided adversarial scenarios, which is far stronger than conventional testing but does not constitute a proof of absence.

06 Conclusions

The bottleneck was never the model's raw capability. It was the absence of a check the model could not negotiate with. Once that check exists — a proof kernel, a global invariant, a threat model rendered machine-readable — autonomy stops being a liability and becomes leverage, because every generated artifact is born already measured against something it cannot argue its way past.

CCC and FastRender were not failed experiments. They were revealing ones. Their test suites were genuine — 8,421 GCC torture-test cases, 94% of the WPT static-layout suite — and the agents passed them all. What they could not pass was what came after: a fuzzer that had no interest in the test suite, and a concurrent scheduler that exposed the deadlock the mutex syntax was only pretending to prevent.

Those failures were not isolated cases. They were the inevitable consequence of operating in a large enough search space so that the protection given by testing is not enough.

The implication is not that agentic code generation approach is broken — it is that the definition of "correct" has to be held by something the agent cannot rewrite. Engineering discipline has always been about constraining the search space; formal methods extend that discipline to the machine doing the searching. SYNVER, Clever, and Agora did not succeed because their models were stronger.

They succeeded because they played a stronger specification/validation/verification game.

References

• He, H., Miller, C., Agarwal, S., Kästner, C., & Vasilescu, B. (2026). "Speed at the Cost of Quality: How Cursor AI Increases Short-Term Velocity and Long-Term Complexity in Open-Source Projects." MSR '26. arXiv:2511.04427.
• Liu, X., Song, S., Zhang, Z., Lan, H., Zeng, J., Wu, M., Heinrich, M., Sun, Y., & Zhang, C. (2026). "Agora: Toward Autonomous Bug Detection in Production-Level Consensus Protocols with LLM Agents." ICML 2026. arXiv:2605.29910.
• Software Improvement & Architecture Review (2026). "State-Space Explosion and Maintainability Rot in Fully Agentic Rendering Engines: A Post-Mortem on FastRender." Journal of Empirical Software Quality, 14(2), 112–129.

• Regehr, J. (2026). "Fuzzing Claude's C Compiler: Undefined Behavior, Silent Miscompilations, and Zero-Degree-of-Freedom Programming." John Regehr's Computing Blog.
• Jones, D. (2026). "The Semantic Blind Spot: Investigating Constraint Validation in an LLM-Generated Rust Codebase." The Shape of Code Audit Series.
• Modular Systems Architecture Group (2026). "The Agentic Tar Pit: Why Text-to-Text Compilers Fail Without Unified Intermediate Representations." Modular Architecture Whitepapers.
• Blitzy Concurrency & Performance Labs (2026). "Skeuomorphic Thread Primitives: Analyzing Asynchronous Painting Deadlocks in Agentic CSS Layout Trees." Blitzy Engineering Deep-Dives.

• Varonis Systems Intelligence Group (2025). "Escaping the Layout Sandbox: Input Validation Failures in Agent-Constructed Mojo IPC Transport Layers." Varonis Threat Research Briefs.
• Anthropic Security Operations (2026). "Project Glasswing: Vulnerability Discovery and Mitigation Dynamics in Evolved Codebases." Anthropic Technical Reports.