AI Agents

This monograph synthesizes 164 scholarly works, 100 practitioner records, and 29 benchmarks to argue coding agents are evaluated as models but deployed as systems — and that many apparent model failures actually originate in the harness, retrieval, state management, or observability. It contributes a versioned catalog of 206 reliability records (193 gated practices, 56 developed in depth), an evidence ledger, and runnable protocols. The framing of evaluation as a dependency chain where one weak layer invalidates downstream conclusions is genuinely useful.

Twin has a frontier coding agent write an executable world model for unknown games like ARC-AGI-3, then enforces via a replay-validation harness that no action is taken until the program reproduces every previously observed transition; each mismatch becomes a counterexample that repairs the model. Results are strong: 179/183 levels cleared (97.8%), goal inferred before any reward on 87.2%. The harness lifts the same base model from 7.8% played directly to 93.3%. The counterexample-driven repair loop is the transferable idea.

This paper reinterprets ACID for agent execution: Semantic Atomicity, Consistency, Isolation, and Durability as guarantees over long-horizon, tool-using workflows on persistent state. The instantiation — a data agent using transactional exploration-execution-validation cycles, confidence-divergence validation, and semantic dependency-aware isolation — reports a 10.6% improvement over state-of-the-art agents including Claude Code. The database-borrowed framing is the strongest part; treating concurrent agent actions as transactions with rollback and isolation semantics is a principled answer to the durability problem.

HELIX treats the runtime harness — not just the model — as something to evolve, decomposing agent systems into typed ports, reusable atoms, recipes, product shells, and runtime policies with traceable provenance. The loop: build harnesses for a fixed model, harvest verified sibling trajectories, update the model, rebuild. On code repair, one evolution round improved task coverage 4.0% over a baseline, and the full 65-candidate portfolio exposed up to 58.0% more verified coverage through complementary behavior, assessed with the SWE-bench evaluator. The auditable-intervention substrate is the contribution.

Vero is the first benchmark to evaluate joint implementation and machine-checked proof synthesis at the repository level: 43 multi-module Lean 4 instances from real repos spanning Python, Dafny, Verus, and Coq, covering cryptographic protocols to distributed systems. Each has curated formal specs and reference implementations supporting proof-only and code-and-proof modes. An audit mechanism lets agents prove specs unsatisfiable or reference code incorrect, which surfaced latent errors during curation — an honest touch. Frontier coding agents are evaluated with full Lean toolchain access.

Anthropic published Claude's system prompts as release notes, drawing 671 points on HN. For anyone reverse-engineering tool-invocation behavior or safety framing, this is the primary artifact rather than a leaked or inferred version — you can read exactly what instructions shape refusal patterns, tool-use conventions, and formatting defaults. Worth diffing against observed behavior in your own integrations, since the documented prompt and the deployed one may drift over time.

MathCode is a mathematical coding agent, surfaced via a project page with 94 points on HN. The linked summary is thin — no benchmark numbers, ablations, or architecture details are visible from the HN entry alone, so treat this as a pointer rather than a validated result. The interesting question for practitioners is whether it treats math as code generation to be executed and checked, or as symbolic reasoning inside the model.

Willison runs Qwen 3.8 27B (Apache 2, vision-capable) locally on an M5 Max MacBook Pro and a DGX Spark via LM Studio's 17GB Q4_K_M build. The self-reported benchmarks claim gains over both Qwen 3.6 27B and the closed Qwen 3.7-Plus, pending independent confirmation. The practical catch: the model defaults to xhigh reasoning effort and spends absurd token budgets over-thinking simple prompts. 27B remains a sweet spot for laptop-class inference.