Formal Specifications & Coding Agents

Uses strongest-postcondition semantics to derive formal abstractions from existing code as the basis for reverse engineering.

Why it matters The oldest item in this map, naming the code-to-specification direction decades before it became a prompt.

Encodes Event-B models into Alloy so a SAT-based finder can search for invariant counterexamples the prover cannot discharge.

Why it matters The clean statement of prove-it versus find-a-counterexample, the tradeoff every agent verification loop re-encounters.

Infers loop invariants by weakening the loop's postcondition, using heuristics such as uncoupling.

Why it matters Pre-LLM statement of the idea the invariant section keeps rediscovering: an invariant is a weakened postcondition, so specification quality bounds invariant quality.

Introduces Dafny, an imperative language whose SMT-backed verifier checks preconditions, postconditions, loop invariants and termination as part of the build.

Why it matters The verification-aware language most of the agent work here targets. Read it to know what 'the verifier accepted it' actually asserts.

TLAPS is the proof system for TLA+, with declarative hierarchical proofs discharged through SMT solvers and proof assistants.

Why it matters The proof half of TLA+, which the natural-language-to-TLA+ work below mostly leaves implicit.

A feature-by-feature tour of Dafny: pre- and postconditions, assertions, loop invariants, termination metrics, quantifiers, predicates and framing.

Why it matters The cheapest way to pick up the specification vocabulary the LLM papers assume you already have.

Tutorial on Frama-C value analysis, deductive verification (WP) and runtime verification (E-ACSL), worked on real Contiki operating-system modules.

Why it matters ACSL annotations are the output target for several spec-generation papers here; this is where that annotation discipline comes from.

Studies 2,300 methods across seven Java libraries and finds the strongest-postcondition transformer yields postconditions too unwieldy to use, motivating a different inference algorithm.

Why it matters Empirical warning that a formally correct specification can still be worthless, which is the gap spec-quality benchmarks now try to measure.

Learns postcondition assertions from observed executions through an evolutionary search over candidate predicates.

Why it matters Dynamic specification mining as it stood before language models, and the implicit baseline that LLM inference is compared against.

Automatically translates SML programs and their function contracts into Coq specifications and proof obligations.

Why it matters Contracts-to-proof-obligations as a compilation problem; the same pipeline shape Coins later exploits to grade generated specifications.

Builds a big-step semantics for an imperative Dafny subset plus a verified verification-condition generator and compiler, after soundness bugs were found in both existing tools.

Why it matters The verifier is part of the trusted base. If an agent's only oracle is a checker with soundness bugs, the guarantee is smaller than it reads.

Observational study of how expert developers actually build proofs in F* and Verus, and where the process stalls.

Why it matters The human baseline for proof-oriented programming, worth having before claiming an agent replaces it.

Traces the evolution and integrations of ESBMC across two decades of bounded model checking for software.

Why it matters Grounds the current wave in the tool lineage it plugs into; several invariant papers below use exactly this substrate.

Generates tick-indexed proof obligations from synchronous programs and LTL assume-guarantee contracts through the automata-theoretic reduction.

Why it matters Concrete machinery for turning a temporal contract into something a first-order backend can actually discharge.

Kani, an open-source bounded model checker for Rust that targets unsafe-code soundness, functional correctness and panic freedom rather than bug-finding alone.

Why it matters Shows what a mainstream-language verifier gives you without writing proofs, which is the baseline agent-written proofs have to beat.

Turns natural-language intent into formal postconditions and evaluates them both for soundness and for power to discriminate buggy programs.

Why it matters Introduced the two axes everything since is graded on: is the specification correct, and does it actually exclude wrong code.

Decomposes a program, generates specifications per sub-component with an LLM, and validates each against the program verifier (AutoSpec).

Why it matters One of the first pipelines to make specification synthesis compositional instead of whole-function guessing.

Measures how well LLMs write VeriFast specifications, where separation-logic auxiliary annotations dominate the actual work.

Why it matters Separation logic is the hardest realistic target in this map, so this is the honest difficulty reading.

Drives specification synthesis from potential runtime errors so large programs can be verified without hand-written contracts.

Why it matters Takes the properties to prove from what the analyzer already fears rather than from a human wish list, which is what makes it scale.

Pushes past postconditions to full contracts, including the preconditions and frame conditions automatic verification needs.

Why it matters Postconditions alone rarely make a verifier succeed; the missing preconditions are where verification stalls.

A dataset of C++ programs paired with LLM-created formal specifications.

Why it matters One attempt to manufacture the training data whose absence KBSpec names.

Pairs symbolic execution with an LLM so path constraints ground the generated program specifications.

Why it matters Representative of the dominant recipe in this section: the model proposes, a sound analysis constrains.

Controlled experiment on LLMs writing Alloy formulas from natural language, repairing faulty formulas, and judging equivalence.

Why it matters Separates three abilities usually measured as one: write, repair, and check.

An agent loop that synthesizes separation-logic specifications, iterating against verifier feedback.

Why it matters The agentic framing applied to the least forgiving specification language here.

Follow-up empirical study of LLM-generated VeriFast specifications on larger heap-manipulating code.

Why it matters Shows where the failures concentrate once the toy functions are gone.

Synthesizes ACSL specifications by combining an LLM with code-property-graph static analysis (AutoACSL).

Why it matters Static analysis used as the retrieval mechanism for what the annotation is obliged to mention.

Generates specification and verification annotations from code with LLMs, then cross-checks them against test oracles.

Why it matters Tests as the cheap oracle for whether a specification is plausible, the same lever Coins formalizes with proof obligations.

Systematically studies which logical constructs (quantification, nesting, frame conditions) LLM-generated specifications actually contain.

Why it matters Aggregate pass rates hide that most generated specifications are shallow; this measures the shallowness directly.

Evaluates LLM-written ACSL annotations for Frama-C deductive verification.

Why it matters The C-side counterpart to the Dafny and Verus results, on the annotation language industrial C verification actually uses.

Studies at scale whether LLMs can write formal program specifications in Rocq, against curated human-written specifications for HumanEval problems.

Why it matters The paper this explorer was built around. It puts the specification, not the code, under test.

Improves dynamic specification inference by having an LLM propose counterexamples that kill candidate invariants overfitted to the observed runs.

Why it matters Counterexamples are where models add most to classical mining: they can imagine executions the test suite never produced.

Builds an evolving domain knowledge base so specification generation is not capped by the scarcity of formal-language corpora (KBSpec).

Why it matters Names the data problem underneath this whole section: there is very little formal specification text to learn from.

Generates Alloy specifications from requirements documents and from production source, then derives executable tests from them.

Why it matters Declarative specifications used to produce tests instead of proofs, a cheaper way into real codebases.

Neuro-symbolic generation and validation of function specifications that reason about the heap as well as about values.

Why it matters Heap-manipulating code is where naive specification generation quietly falls apart.

Synthesizes and then refines formal specifications for real-world program verification with the model in the loop (SpecSyn).

Why it matters Refinement rather than one-shot generation is what lets specifications survive contact with real code.

Plain-language abstract Spec-Driven Test Generation has an LLM agent first write a semi-formal specification of a code component's pre-conditions, post-conditions, and undefined behaviors, then use that specification as a scaffold to generate tests, instead of generating tests directly from code.

Motivation Agents prompted to generate tests directly from code often fail to reason about the code's underlying contracts, missing edge cases and behavioral boundaries. Design by Contract has long formalized this reasoning for humans via pre-/post-conditions and invariants, but agents generating tests have no such explicit contract to anchor exploration, so they can hallucinate logic or generate superficial tests.

Methodology A two-phase Spec-Driven Agent first retroactively extracts and documents a component's contract as a semi-formal (natural-language-structured, not mathematically formal) specification, then generates tests grounded in that document. It is compared against a baseline agent that generates tests directly, on 90 historical production bugs from Google's issue tracker, using a 'Greenfield Test Generation' setup. A novel Contract Coverage metric scores how completely a spec covers a bug's incorrect behavior, and a pairwise LLM-as-a-Judge (Gemini 3.1 Pro judging outputs from agents using Gemini 3 Flash) rates test suite quality.

Results The Spec-Driven Agent reaches a 63.2% bug detection rate at k=5 runs, a statistically significant 9.8-percentage-point improvement over the baseline (p=0.0352), and a 2.5-percentage-point improvement in branch coverage (p=0.0034). The LLM judge rates its test suites superior to the baseline's in 77.8% of cases and to human-authored tests in 56.7% of cases, with gains in adherence to best practices, readability, and edge-case coverage.

Prompts LLMs for inductive loop invariants and checks each candidate with a verifier, solving instances classical tools miss.

Why it matters The result that opened this line. Invariant inference is guess-and-check, and models are unusually good guessers.

Formalizes LLM-plus-automated-reasoner program verification as a set of sound proof rules, so model proposals cannot make the system unsound (Lemur).

Why it matters The soundness discipline the rest of this section depends on, stated explicitly rather than assumed.

Trains a re-ranker over LLM-generated invariant candidates so the correct one is checked early.

Why it matters Generation is cheap and checking is expensive, so ordering the candidates is most of the speedup.

A loop-invariant benchmark built from programs that manipulate memory rather than numbers.

Why it matters Most invariant results are on numeric loops; this is the harder and more realistic distribution.

Targets invariant generation for programs whose complexity defeats template-based tools.

Why it matters Useful for seeing which program features, not which prompts, decide success.

Replaces loop unrolling in bounded model checking with a control-flow-graph node asserting an LLM-generated invariant.

Why it matters A clean integration point, where the model supplies precisely the piece the classical algorithm lacks.

Extends the same guess-and-check approach from safety invariants to ranking functions for termination.

Why it matters Termination is the half of correctness that agent papers routinely skip.

Generates invariants by reasoning backward through weakest-precondition semantics instead of pattern-matching the loop body.

Why it matters Ties the modern pipeline back to the calculus in the foundations section.

Couples reasoning-tuned LLMs with SMT solvers for loop invariant generation.

Why it matters A current reading on how much reasoning training changes the guess half of guess-and-check.

Accelerates program verification by synthesizing the invariants that let the verifier discharge its goals faster (Quokka).

Why it matters Invariant quality shows up as verifier runtime, which decides whether verification fits inside a build.

Combines contract inference with loop invariant synthesis so verification scales past a single function (ConVer).

Why it matters Contracts and invariants are the same problem at two granularities, and this treats them together.

Has the model write a step-by-step natural-language proof, formally checks that reasoning, and feeds back the local errors.

Why it matters Feedback on the reasoning rather than on the final artifact, a different loop shape from verifier-only iteration.

Uses deductive feedback to synthesize invariants for programs with interacting loops (InvWeaver).

Why it matters Interacting loops break per-loop synthesis, which is exactly where most tools stop.

Curates training data so small models learn to produce the invariants that actually help the verifier.

Why it matters Evidence that this task does not need a frontier model when the data is chosen well.

Showed that few-shot LLMs translate natural-language mathematics into formal statements at non-trivial rates.

Why it matters The origin point for treating formalization as translation; every requirements-to-specification paper here inherits the framing.

Interactively translates unstructured natural language into temporal logic, letting the user correct sub-translations rather than the whole formula (nl2spec).

Why it matters Human-in-the-loop translation with a fine-grained repair unit, still the most practical interface shape for this task.

Evaluates LLM-driven user-intent formalization for verification-aware languages, separating soundness of the formalized intent from its completeness.

Why it matters The clearest statement of why intent formalization is its own evaluation problem, distinct from code correctness.

Short survey of formalizing software requirements with LLMs.

Why it matters A compact entry point that separates requirements formalization from mathematical autoformalization.

Survey of autoformalization in the LLM era: targets, training signals, and how results are evaluated.

Why it matters The map of the subfield, and a good way to see how little of it evaluates semantic fidelity.

Decomposes industrial requirements through hierarchical semantics before mapping them to LTL (Req2LTL).

Why it matters Decomposition is what keeps a long requirement from collapsing into one confidently wrong formula.

Paraphrases the same statement in meaning-preserving ways and measures whether the formalization stays the same.

Why it matters If a paraphrase changes the formula, the translation was not tracking meaning. Cheap to run and hard to argue with.

Evaluates LLMs end to end on turning natural-language requirements into verifiable formal proofs.

Why it matters Connects the translation problem to the proof problem instead of stopping at a well-formed formula.

A multi-agent vision for developing and formalizing requirements before any code is generated.

Why it matters Positions requirements engineering, not prompt engineering, as the reliability lever.

Generates LTL specifications from industrial aerospace requirement documents.

Why it matters Real requirements, with the domain vocabulary and messiness that benchmark sentences lack.

Translates unstructured requirements into linear temporal logic with LLMs.

Why it matters A current data point on the least structured input the task has to handle.

First systematic evaluation of whether LLMs produce semantically correct TLA+ from natural language.

Why it matters TLA+ carries real industrial use at Amazon and Microsoft, so the gap measured here is a gap in practice.

An agent that asks clarifying questions before committing to a signal temporal logic formula.

Why it matters Ambiguity in the requirement, not weakness in the model, is often the real blocker.

An agent that synthesizes and repairs Event-B formal models.

Why it matters Refinement-based modeling, where the specification is the primary artifact and code arrives later.

Uses selective conformal prediction with semantic verification so the translator abstains instead of emitting an unreliable specification.

Why it matters Abstention is the underused answer to the fidelity problem: not every requirement should be formalized automatically.

Preference-optimized low-rank adaptation for synthesizing TLA+ specifications that check out.

Why it matters Training rather than prompting for the same task, which is where the cheap wins have moved.

Plain-language abstract Agent skills are prose procedure files loaded into a model's context and interpreted by a tool-calling loop, which means nothing in the runtime makes a mandated step happen. Measured against the procedures their own skills prescribe, a prose agent performs 56% of mandated steps on gpt-4o while still producing deliverables that pass output checks. SIGIL compiles a SKILL.md into an executable harness through a typed intermediate representation that marks each step as owned by code or by the model, raising step compliance to 86%, full-procedure completion from 28% to 65% of runs, and cutting median token cost to 0.58x.

Motivation Skills succeeded as an authoring format because domain experts can write, review and version them, but the property that makes them accessible leaves them unenforced. The document is consulted by the same process that is supposed to obey it, so an agent can satisfy its own reading of an instruction by writing a sentence asserting the outcome. Hand-writing a harness fixes enforcement at the cost of the authoring surface, and leaves two independent representations of one procedure free to drift. The resulting defect class is invisible to artifact-level testing: a financial-compliance report can carry reasonable figures and conclusions and still be invalid if the agent never retrieved the authoritative records, recalculated the totals, or checked the result against policy. Prior runtime supervision work adds monitors and guards that can block a disallowed action, but detection does not make a required action occur.

Methodology Compilation runs in two stages over AG-IR, a typed agentic IR whose nodes carry an owner stating whether code or the model executes the step, a modality recording how binding the source instruction was, and provenance to the mandating sentence. Extraction is the only stage containing a model and admits a rule only when a verbatim quotation supports it; six compile gates then reject an IR that points at content instead of embodying it, omits a mandated deliverable, fails to lower and type check, folds a mandatory rule into another slot's interior, or leaves a human-gated decision to model judgment. Lowering is deterministic, mapping each primitive onto an Object-Spatial Programming construct in Jac: nodes become node archetypes, edges fix walker traversal order, mandatory rules become abilities bound to node entry, model-owned nodes become typed llm() slots whose return type makes an out-of-range answer a type error, and forbidden rules lower to nothing, so the guarantee comes from the absence of a path. STRUCT-COV statically reports, per mandatory rule, whether the emitted module realizes it as a code gate, a dedicated model slot, monolithically inside another slot, or not at all, failing the last two. Evaluation covers 30 skills across document and tooling, software process, and governance and compliance families, with three process-scenario tasks per skill repeated three times per arm in isolated sandboxes, on gpt-4o and gpt-5, scored by Applicable-Mandate Compliance with a judge reading the full run and, for the harness, its node-path trace.

Results On gpt-4o the compiled harness performs 86% of mandated steps against 56% for prose, matching or exceeding prose on all 30 skills with 28 strict wins, 2 ties and no losses, and completing the full applicable procedure in 65% of runs against 28%, a factor of 2.3. Moving to gpt-5 leaves the harness at 86% while prose rises to 68%, so the advantage narrows from 30 points to 17; the harness artifact is byte-identical across both sweeps, which is what makes the guarantee model-independent by construction. Median token cost is 0.58x prose, cheaper on 24 skills and as low as 0.02x on a nearly all-code skill, with the exceptions concentrated in skills organized around a genuine tool-using loop, reaching 7.64x on using-superpowers and 3.09x on systematic-debugging, where the prose agent was cheaper because it truncated or skipped the loop. The compiler realizes 37% of mandates as code-owned gates on average, 32% to 44% by family, and the four skills where the harness loses on gpt-5 are judgment-heavy ones with little to compile.

Closes the loop by checking code, specification and documentation against each other before accepting a generation (Clover).

Why it matters Consistency between artifacts as an acceptance criterion, which catches the case where code and specification are both wrong together.

Closed-loop PLC code generation and verification for industrial control systems (Agents4PLC).

Why it matters Safety-critical control code is a domain where verification is already mandatory, so the loop has a real customer.

Bootstraps verified Verus code by translating from a source language and refining against the verifier (Treefinement), with no human proof data.

Why it matters Self-improvement where the reward is a real verifier, the cleanest version of verifiable rewards in this space.

Generates Verus proof annotations for Rust with a pipeline modeled on how humans construct proofs.

Why it matters The reference point for automated proof generation in the Rust ecosystem.

Combines LLM code generation with formal specifications and reactive program synthesis.

Why it matters Pairs a generator with a synthesizer that is correct by construction, splitting the work by what each is good at.

Synthesizes verified Dafny methods, generating specification and code together so the pair can be proved.

Why it matters An early, careful statement of the generate-spec-and-code-together strategy that most later systems adopt.

Guides Monte Carlo tree search with a Dafny or Coq verifier to synthesize multi-step verified programs (VerMCTS).

Why it matters Uses the verifier as a partial-credit signal inside search rather than only as a final gate.

Combines a language model with search to add the logical annotations Dafny needs to verify a program (dafny-annotator).

Why it matters Isolates annotation from code generation, which is the part that actually costs developer time.

Generates Dafny as an intermediate language, verifies it, and compiles from there to the target language.

Why it matters Verification as a compilation stage rather than a separate discipline, and one of the more transferable ideas in this section.

Uses retrieval-augmented generation and context-aware prompting for multi-module proof synthesis, with RepoVBench as the yardstick (RagVerus).

Why it matters Retrieval as the answer to repository-scale context, plus the first repository-level Verus benchmark.

Reduces human annotation in formal software verification by training with reinforcement learning against Dafny's verifier.

Why it matters Formal-language reasoning as a reliable and scalable training signal, in contrast to informal-language reward models.

Repairs arithmetic errors in Dafny programs under the guidance of the existing specification.

Why it matters Repair with a specification present is a very different problem from repair against tests, and much better posed.

Resolves cross-module dependencies and global context for repository-scale program verification.

Why it matters Function-level results do not transfer to repositories, and this states why.

Explores using SPARK for Ada to verify LLM-generated code.

Why it matters Ada/SPARK is where high-assurance industry already lives, so it is a realistic adoption path rather than a research language.

Evaluates vericoding in Lean and develops agent-guided search methods over the space of verification attempts.

Why it matters Verification failure is cheap to detect and expensive to fix, which makes search a natural fit for the loop.

Agentic verified code generation in Dafny.

Why it matters A recent read on what the agent loop adds over single-shot generation in a verification-aware language.

Adds a diff-checker, an invariant pruner and retrieved proof strategies at inference time for Dafny verification (DafnyPro).

Why it matters The diff-checker matters beyond Dafny, because it stops the model quietly editing the program it was asked to prove.

Turns failed proofs into concrete counterexamples so the model reasons about behavior rather than about verifier text (ExVerus).

Why it matters Verifier error messages are weak feedback; counterexamples are the strongest signal the tool can give back.

Hoare-style decomposition that lets formal methods reach large systems (FM-Agent).

Why it matters Decomposition is the scaling story for deductive verification, and this is a concrete instance of it.

Closes the verification loop on AI-generated safety-critical software through model-driven engineering.

Why it matters One of the few papers taking the vibe-coding workflow seriously and asking what formal gate belongs inside it.

Scalable and resilient proof generation for Rust code across large, evolving systems (KVerus).

Why it matters Focuses on proof maintenance under change, which is where verification effort actually accumulates.

Generates Kani specifications for unsafe Rust and assesses their quality rather than assuming code-derived specs are right (KaPilot).

Why it matters Specifications derived from an implementation inherit its bugs, and this confronts that directly.

Scales specification writing so a model checker can be run autonomously over systems code (Specula).

Why it matters Targets the real bottleneck in model checking, which is the specifications it needs rather than the checker.

Targets the intermediate executable assertions a programmer relies on mid-algorithm, after finding that prompted assertions are often invalid, trivial, or too weak to reject a behavior-changing fault.

Why it matters Specification as a reasoning scaffold rather than a downstream deliverable, and a clean statement of how weak default generated assertions are.

Coding agents producing verified security software in Ada/SPARK, with the prover as the acceptance criterion.

Why it matters Makes the verifier the judge of agent output, which is the strongest available form of automated review.

LLM-driven theorem proving applied to the seL4 verified microkernel.

Why it matters The most demanding real target available, with industrial scale and existing human proofs to compare against.

A cross-system benchmark of 488 Olympiad-level formal statements across Metamath, Lean, Isabelle and HOL Light (miniF2F).

Why it matters The standard yardstick for prover capability. It is mathematics, so treat transfer to software verification as an open question rather than a given.

Generates whole proofs with a language model and repairs them using the proof assistant's error messages (Baldur).

Why it matters Established whole-proof generation plus repair as an alternative to single-tactic prediction.

Extracts a Lean dataset and provides retrieval-augmented premise selection with an interactive proving environment (LeanDojo).

Why it matters The infrastructure a large share of neural proving work is built on.

371 undergraduate mathematics problems with paired informal and formal statements for autoformalization and proving (ProofNet).

Why it matters The benchmark that made autoformalization measurable, and the template later software-specification benchmarks copy.

Divide-and-conquer proof automation that accepts partial progress toward a Coq proof (Cobblestone).

Why it matters Partial proofs are useful; treating verification as all-or-nothing throws away most of the work.

Scales formal proving with large-scale synthetic data generated by autoformalizing informal problems (DeepSeek-Prover).

Why it matters Showed that the data bottleneck in formal proving is partly solvable by generation.

A dataset for training models on Coq code.

Why it matters Training data for proof assistants is scarce and idiosyncratic; this is one of the open corpora.

Runs LLM inference natively inside Lean for tactic suggestion, premise selection and proof search (Lean Copilot).

Why it matters The interactive framing, where the model is a copilot inside the prover rather than a prover itself.

Retrieval-augmented proof synthesis that adapts to the project's own lemmas and proof style (Rango).

Why it matters Proof automation is project-specific, and retrieval is what makes it so.

Automated proof for software verification in Isabelle, built on a project-scale corpus (Selene).

Why it matters One of the first attempts at software, rather than mathematics, as the proof-automation target.

A minimalist proof language for neural theorem proving over Isabelle/HOL.

Why it matters Changes the target language to fit the model rather than the other way around.

Reinforcement learning over subgoal decomposition for formal mathematical reasoning (DeepSeek-Prover-V2).

Why it matters The current capability ceiling for open proving models, and the reference point when a software-verification agent claims strong results.

Augments theorem proving by combining LLM-driven proof synthesis with refinement (HybridProver).

Why it matters Synthesis and refinement as separate stages, mirroring the generate-then-repair pattern in verified code generation.

Case study of agentic proof automation, where the model explores the codebase rather than seeing one goal at a time.

Why it matters Proof engineering is a codebase task, and this is what changes when the agent can look around.

Contract-aware proof repair for Isabelle, with an independent checker enforcing a machine-readable edit contract and retained audit records (CAPRI).

Why it matters A build that succeeds does not show the model changed only what it was authorized to change; this closes that hole.

Pilot study of whether open-weight models can produce kernel-verified Coq proofs.

Why it matters Resemblance to a proof is not a proof, and the kernel is the only judge that settles it.

Measures and optimizes the cost-quality tradeoff of agentic theorem provers in Lean, where much compute is spent on attempts that never land.

Why it matters The economics paper this area needs, since proof search is easy to make expensive and hard to make cheap.

Proof automation framed as structural imitation of how humans reason (PROMISE).

Why it matters An argument that proof structure, not token-level tactic prediction, is the transferable unit.

Difficulty-aware decomposition for automating Rocq proofs.

Why it matters Spends proof-search budget where the goal is actually hard, which is most of the cost control in agentic proving.

Coins scores a candidate specification by instantiating it on trusted test cases and generating concrete proof obligations, so a spec is graded by what it actually rules out.

Why it matters Moves specification evaluation past 'does it typecheck' and past 'does it resemble the reference', which is the measurement missing from most generation work here.

Over 750 Dafny programs, about 53,000 lines, testing whether a model can supply enough hints for the verifier to succeed.

Why it matters The largest Dafny yardstick, and the one most later Dafny systems report against.

A minimal benchmark for proving properties of code in Lean (miniCodeProps).

Why it matters The smallest honest bridge between mathematical proving benchmarks and software properties.

A benchmark for vericoding: formally verified program synthesis from specifications.

Why it matters Names the task cleanly and separates it from proof-only and code-only evaluation.

A curated benchmark for formally verified code generation with human-checked ground truth (CLEVER).

Why it matters Small and hand-verified rather than large and noisy, which is what makes its numbers interpretable.

Evaluates LLM reasoning about program semantics through formal specification inference (FormalBench).

Why it matters Treats specification inference as a probe of semantic understanding, which reframes what a failure means.

Applies mutation testing to Dafny specifications to reveal weaknesses in the specifications themselves (MutDafny).

Why it matters Specifications are as buggy as implementations, and mutation is the cheapest way to see it.

Specification generation for operating-system verification (OSVBench).

Why it matters Systems code with real invariants, far away from the function-sized tasks most benchmarks use.

Formally verified code generation over competitive-programming problems in Lean (FVAPPS).

Why it matters Takes a familiar code benchmark and raises the bar from passing tests to carrying a proof.

Benchmarks verifiable code generation on Lean tasks that require code, specification and proof together, each graded separately (VERINA).

Why it matters Separating the three deliverables is what exposes systems that write code well and specifications badly.

Validates formal specifications with LLM-generated test cases.

Why it matters Tests as a validity check on the specification inverts the usual direction and is a practical review technique.

Scores formally verifiable code by equivalence rather than against a reference solution (VeriEquivBench).

Why it matters Ground-truth-free evaluation matters because there is rarely one right specification.

Requires code, specification and proof to be produced at once, following the VerifyThis competition format.

Why it matters The joint task is much harder than any of its parts, and this measures the joint task.

An aligned benchmark for verified code generation on classical algorithms (AlgoVeri).

Why it matters Algorithms with known invariants make a good controlled setting for comparing systems.

Evaluates code-derived and LLM-written specifications on a production point-of-sale payment workflow, grading them against traces captured from the running system.

Why it matters Finds reliability governed by the structure of the specification contract rather than by the specification language, and reframes the economics of having a model at all.

Evaluates Rust verification through the chain of reasoning rather than binary pass or fail on proof hints (VCoT-Bench).

Why it matters Pass rates hide whether the model understood the proof obligation or got lucky.

Benchmarks formal translation across interactive theorem provers (ITPEval).

Why it matters Cross-prover transfer is a good test of whether a model learned the mathematics or the syntax.

A live benchmark of agentic workflows on specification generation (LiveFMBench).

Why it matters Live construction is the current defense against contamination, which quietly inflates every static benchmark here.

Benchmarks formal postcondition inference on both correctness and completeness rather than correctness alone.

Why it matters A postcondition that is true but weak passes most evaluations; completeness is what catches that.

Grades natural-language-to-TLA+ generation by running the model checker over the full reachable state space, not by resemblance to a reference (TLA+-Bench).

Why it matters Execution-grounded grading is the correct answer to 'does it parse' and 'does it look like the gold spec'.

Asks whether agents can build formally verified software repositories, not single functions (Vero).

Why it matters Repository scale is where specification, proof and engineering all have to hold at once.

An agentic environment for evaluating specification autoformalization in Verus (Verus-SpecGym).

Why it matters Environment rather than static dataset, so agent behavior is part of what gets measured.

Plain-language abstract A benchmark for whether agent-generated reproduction code implements what a paper actually specifies, judged claim by claim without running anything. Thirty ICLR, ICML and NeurIPS 2025 papers are decomposed into 1,491 human-verified Semantic Alignment Units: atomic implementation claims, each traceable to a paper span and checkable by reading code. Claims are typed into four kinds of drift (numerical, method or formula, experimental protocol, step ordering) and scored on a five-level rubric by an LLM judge. Twelve generator configurations, four models by three scaffolds, are evaluated over all thirty papers.

Motivation Paper-to-code reproduction asks an agent to produce a repository that is not merely executable but faithful to a paper's algorithmic logic, numerical details, experimental protocol and execution order. Two properties make that hard: papers are written to communicate findings rather than prescribe implementations, so the method sits in one section and the hyperparameters in an appendix table, and scientific code is intolerant of detail-level error, where one misread formula changes the implemented method while the code still runs. The authors name the resulting failure semantic drift, generated code silently diverging from the paper's specifications. Evaluating it is awkward because there is no executable ground-truth oracle: unlike SWE-bench, where a test suite states expected behavior, the only authoritative specification is the paper text, and end-to-end numbers are confounded by seeds, environments, data processing and compute budget. Existing reproduction benchmarks report pass/fail or scalar scores at document or function level, so when reproduction falls short the deviation is never classified.

Methodology Extraction runs as a staged agent pipeline followed by mandatory human review. A code-first filter removes non-implementable content without an LLM call, then three dimension-specific specialist agents process the paper in parallel, each dispatching per-section sub-agents that read one to three sections at a time to avoid long-context attention decay; a merge stage deduplicates and derives step-ordering claims from annotations the other agents recorded rather than from a separate pass. The pipeline is tuned for recall, and human reviewers accept, revise, reject or split each candidate against contribution relevance, drift-type correctness, granularity and source precision, logging the reasoning; about 17% of candidates are rejected. Scoring is static: a GPT-5.5 judge, distinct from all generators to avoid self-evaluation bias, searches the generated repository for evidence, drops claims with no code-level support, and scores the rest on the five-level rubric with a structured explanation and file-and-line citations. The paper-level score is the mean over its SAUs. Generators are Claude-Sonnet-4.6, DeepSeek-V4-Pro, Gemini-2.5-Flash and GPT-4o under three scaffolds: a minimal ReAct loop, a dedicated three-role paper-to-code pipeline, and a software-engineering execution-feedback scaffold.

Results Performance is uniformly low. Across 360 paper-level evaluations the mean alignment score is 0.221 with a median of 0.237; the best single configuration, Claude-Sonnet-4.6 with PaperCoder, reaches 0.301. Of 17,892 claim judgments, 7,034 score zero, and three categories cover most of them: implementation mismatch at 40.8%, where code referencing the claim's keywords implements something else; stubs, TODOs or pass statements at 16.2%; and external knowledge gaps at 8.0%, where the paper names a standard baseline or dataset without defining it. The dimension ordering numerical > algorithm > ordering > protocol holds across all twelve configurations, tracking the number of sub-decisions each claim type demands, with protocol claims the universal bottleneck. Model choice outweighs scaffold choice on average (model marginal range 0.120-0.283 against 0.193-0.249 for scaffolds), and scaffold benefit shrinks as base capability rises: the paper-to-code scaffold adds 0.116 for GPT-4o and 0.106 for Gemini-2.5-Flash but 0.029 for Claude and -0.027 for DeepSeek. Domain effects are small next to generator effects, a spread of 0.030 against a 0.219 gap between best and worst configuration. The judge agreed with human assessment on about 87% of 200 re-checked claims.

Studies whether LLMs can write good property-based tests, including inventing the properties.

Why it matters Properties are lightweight specifications, and this is the honest read on the model's ability to invent them.

Plain-language abstract SWE-bench is a benchmark for testing whether language models can solve real software engineering problems. It presents models with 2,294 actual GitHub issues from 12 popular Python repositories and asks them to generate code patches that fix those issues, verified by running the repository's own test suite.

Motivation Existing coding benchmarks like HumanEval consist of self-contained problems solvable in a few lines, which no longer capture what frontier language models can and cannot do. Real software engineering requires navigating large codebases, understanding interactions across many files, and reasoning about complex bugs — a much harder and more realistic challenge that prior benchmarks did not test.

Methodology The authors scraped pull requests from 12 popular Python repositories, filtered for PRs that resolved a linked GitHub issue, included changes verified by tests that shifted from failing to passing, and excluded instances with installation or runtime errors. This pipeline reduced roughly 90,000 PRs to 2,294 curated task instances. Models are given an issue description and a codebase snapshot, and must produce a patch; evaluation uses BM25-based retrieval to provide relevant context and runs the repository's test suite to check correctness. The authors also released a training set of 19,000 instances from 37 repositories and two fine-tuned models, SWE-Llama 7b and 13b, built on CodeLlama.

Results State-of-the-art models performed very poorly on SWE-bench. The best-performing model, Claude 2, resolved only 1.96% of the issues when using a BM25 retriever. Fine-tuned SWE-Llama 13b was competitive with Claude 2 in some settings and could handle contexts exceeding 100,000 tokens, but overall results confirm that current language models struggle with realistic, multi-file software engineering tasks.

Shows a simple localize-repair-validate pipeline matches or beats complex agent scaffolds on SWE-bench (Agentless).

Why it matters A standing caution against attributing to agency what belongs to the model and the test harness.

Builds a taxonomy of hallucinations in LLM-generated code, past whether tests pass.

Why it matters Names the failure modes formal specifications are supposed to catch, in the vocabulary of the code-generation literature.

Finds that LLM-based test generators validate faulty code rather than finding bugs, by design choice.

Why it matters The oracle problem stated plainly. Tests written from the implementation cannot detect the implementation being wrong.

Generates executable oracles that check client code against the requirements stated in JDK Javadocs.

Why it matters Documentation as an existing specification source, already sitting in most codebases.

Audits SWE-bench and finds solution leakage and weak tests behind a substantial share of reported passes.

Why it matters If the oracle is weak, so is every claim measured through it, which is the case for formal specifications in miniature.

Extracts developer intent from the repository to guide issue resolution and to justify the patch (SpecRover).

Why it matters Intent recovery inside a mainstream agent, meeting the formal-specification work from the other direction.

Quantifies package hallucination in code-generating models as a supply-chain threat.

Why it matters A failure that no functional test catches and no functional specification describes.

Assesses correctness of generated code from the model's internal representations rather than post-hoc checking.

Why it matters A cheap confidence signal for when the expensive verification step is worth running.

Estimates the probability that a generated program is correct without any oracle, using incoherence across samples.

Why it matters The oracle-free setting is the common one, and this is a principled way to act in it.

Scenario-based evaluation of code smells in LLM-generated code.

Why it matters Maintainability is the quality axis that survives long after the tests pass.

Argues automated software engineers should abstain on uncertain inputs instead of always emitting a patch.

Why it matters Abstention as a reliability primitive, matching the conformal-prediction move in the translation section.

Addresses non-functional quality characteristics of LLM-generated code, which functional benchmarks ignore.

Why it matters Correctness is not the only property that ships, and specifications rarely cover the rest.

Predicts functional correctness of generated code through uncertainty quantification.

Why it matters Routes verification effort toward the generations most likely to be wrong.

Empirical study of test-first and agentic workflows where one model both writes and validates the code.

Why it matters Self-validation is the structural weakness in agent loops, and formal verification is one way out of it.

Identifies patch verbosity in agentic program repair, where patches pass tests while doing far more than asked.

Why it matters Passing tests permits large unintended changes, which is exactly what a frame condition would rule out.

Proposes contracts as the missing quality-assurance step in vibe coding.

Why it matters The bridge between the contract literature and the way code is actually produced now.

Plain-language abstract Spec-Driven Test Generation has an LLM agent first write a semi-formal specification of a code component's pre-conditions, post-conditions, and undefined behaviors, then use that specification as a scaffold to generate tests, instead of generating tests directly from code.

Motivation Agents prompted to generate tests directly from code often fail to reason about the code's underlying contracts, missing edge cases and behavioral boundaries. Design by Contract has long formalized this reasoning for humans via pre-/post-conditions and invariants, but agents generating tests have no such explicit contract to anchor exploration, so they can hallucinate logic or generate superficial tests.

Methodology A two-phase Spec-Driven Agent first retroactively extracts and documents a component's contract as a semi-formal (natural-language-structured, not mathematically formal) specification, then generates tests grounded in that document. It is compared against a baseline agent that generates tests directly, on 90 historical production bugs from Google's issue tracker, using a 'Greenfield Test Generation' setup. A novel Contract Coverage metric scores how completely a spec covers a bug's incorrect behavior, and a pairwise LLM-as-a-Judge (Gemini 3.1 Pro judging outputs from agents using Gemini 3 Flash) rates test suite quality.

Results The Spec-Driven Agent reaches a 63.2% bug detection rate at k=5 runs, a statistically significant 9.8-percentage-point improvement over the baseline (p=0.0352), and a 2.5-percentage-point improvement in branch coverage (p=0.0034). The LLM judge rates its test suites superior to the baseline's in 77.8% of cases and to human-authored tests in 56.7% of cases, with gains in adherence to best practices, readability, and edge-case coverage.

Plain-language abstract A repository-level benchmark of 119 scientific software engineering tasks from 98 GitHub repositories across 20 scientific domains, built to ask not only whether coding agents repair scientific code but why they fail when they do not. No agent tested clears 50% exact private-test success.

Motivation Software is part of the instrument through which scientific claims are produced: research groups use it to run simulations, process instrument output, train surrogate models and reproduce published results, so a defective patch can corrupt the evidence behind a conclusion rather than only a program output. Existing coding benchmarks measure function synthesis and repository-level repair, and existing scientific coding benchmarks cover curated problems, paper-grounded implementations, workflows and repository execution, but repository-level coverage across scientific domains and analysis of failure mechanisms remain thin. Aggregate test scores cannot distinguish an incorrect scientific abstraction from superficial symptom repair, incomplete system integration, or a fix that does not generalize, so they give limited guidance on how to improve the agents.

Methodology Each task ships a repository snapshot at the exact pre-task state with locked dependencies and runnable entry points, stripped of git history, remotes, future changelogs, build caches and solution-linked artifacts; a problem statement frozen before test and reference-patch authors saw one another's work; a required scientific context held fixed in every condition; and public tests that support interactive debugging. Private tests, contract labels, reference and alternative-valid patches, scientific-rationale and localization blocks, expected files, difficulty and contamination metadata are evaluator-only and are mounted after submission in a separate container, reachable from neither the workspace nor environment variables nor logs. Tasks are split into Issue-driven (52), Expert-exploratory (49) and Engineering-integration (18) paradigms; hidden validators include alternative execution paths, state-reset tests and inter-module behavioral-contract tests. Metrics are public score, private score, Fail2Pass, Pass2Pass and Pass@1, the last binary and requiring every applicable private test to pass. Eight model-harness configurations were evaluated. Unsuccessful attempts were manually audited into four mutually exclusive scientific failure mechanisms, with runtime or evaluation-path failures recorded separately. A paired ablation on the 91 tasks where scientific auxiliary information can be separated removes scientific principles, equations, expected properties, domain diagnoses and repair strategies while holding the snapshot, environment, public entry points, hidden validators and required context fixed.

Results Public scores run 93.28% to 100.00% while Pass@1 stays under 50% for every configuration. Claude-Opus-5 with Claude Code leads Pass@1 at 47.90% and on both Issue-driven (38.46%) and Expert-exploratory (65.31%) tasks; GPT-5.6-sol with Codex leads private score (78.82%), Fail2Pass (72.30%) and Pass2Pass (97.66%); DeepSeek-V4-Pro leads public score and Engineering-integration (44.44%); Qwen3.5-397B trails at 14.29% overall. No single model leads every metric, and the authors read the spread as a difference in how effectively each model-harness pair uses its context and generation budget rather than in token volume, since Claude-Opus-5 takes the top Pass@1 on a moderate budget and GPT-5.6-sol reaches a similar level with much shorter outputs. In the failure audit, Claude-Opus-5 records the lowest categorized scientific-error count at 58 plus 4 runtime or evaluation-path failures, and the fewest misguided-exploration errors at 2; DeepSeek-V4-Pro records the fewest knowledge/abstraction (15) and integration (19) errors; DeepSeek-V4-flash the fewest generalization errors (6). The ablation shows scientific knowledge is not uniformly beneficial. For GPT-5.6-sol, supplying it raised mean public and private scores slightly (96.70 to 97.80, 73.23 to 74.06) but lowered Pass@1 from 36.26% to 31.87%, with 8 tasks solved only with the information and 12 only without. For DeepSeek-V4-flash the same intervention raised Pass@1 from 16.48% to 23.08% while increasing input tokens from 4.84M to 7.40M. The authors state these are paired descriptive differences establishing neither significance nor causality, and read the GPT cases as scientific information supplying semantic constraints absent from local code symptoms while also inducing anchoring, scope spillover, or premature reliance on a supplied explanation. Stated limitations: per-domain task counts are small, and the analysis of how domain knowledge is actually used remains preliminary.

Plain-language abstract A benchmark for whether agent-generated reproduction code implements what a paper actually specifies, judged claim by claim without running anything. Thirty ICLR, ICML and NeurIPS 2025 papers are decomposed into 1,491 human-verified Semantic Alignment Units: atomic implementation claims, each traceable to a paper span and checkable by reading code. Claims are typed into four kinds of drift (numerical, method or formula, experimental protocol, step ordering) and scored on a five-level rubric by an LLM judge. Twelve generator configurations, four models by three scaffolds, are evaluated over all thirty papers.

Motivation Paper-to-code reproduction asks an agent to produce a repository that is not merely executable but faithful to a paper's algorithmic logic, numerical details, experimental protocol and execution order. Two properties make that hard: papers are written to communicate findings rather than prescribe implementations, so the method sits in one section and the hyperparameters in an appendix table, and scientific code is intolerant of detail-level error, where one misread formula changes the implemented method while the code still runs. The authors name the resulting failure semantic drift, generated code silently diverging from the paper's specifications. Evaluating it is awkward because there is no executable ground-truth oracle: unlike SWE-bench, where a test suite states expected behavior, the only authoritative specification is the paper text, and end-to-end numbers are confounded by seeds, environments, data processing and compute budget. Existing reproduction benchmarks report pass/fail or scalar scores at document or function level, so when reproduction falls short the deviation is never classified.

Methodology Extraction runs as a staged agent pipeline followed by mandatory human review. A code-first filter removes non-implementable content without an LLM call, then three dimension-specific specialist agents process the paper in parallel, each dispatching per-section sub-agents that read one to three sections at a time to avoid long-context attention decay; a merge stage deduplicates and derives step-ordering claims from annotations the other agents recorded rather than from a separate pass. The pipeline is tuned for recall, and human reviewers accept, revise, reject or split each candidate against contribution relevance, drift-type correctness, granularity and source precision, logging the reasoning; about 17% of candidates are rejected. Scoring is static: a GPT-5.5 judge, distinct from all generators to avoid self-evaluation bias, searches the generated repository for evidence, drops claims with no code-level support, and scores the rest on the five-level rubric with a structured explanation and file-and-line citations. The paper-level score is the mean over its SAUs. Generators are Claude-Sonnet-4.6, DeepSeek-V4-Pro, Gemini-2.5-Flash and GPT-4o under three scaffolds: a minimal ReAct loop, a dedicated three-role paper-to-code pipeline, and a software-engineering execution-feedback scaffold.

Results Performance is uniformly low. Across 360 paper-level evaluations the mean alignment score is 0.221 with a median of 0.237; the best single configuration, Claude-Sonnet-4.6 with PaperCoder, reaches 0.301. Of 17,892 claim judgments, 7,034 score zero, and three categories cover most of them: implementation mismatch at 40.8%, where code referencing the claim's keywords implements something else; stubs, TODOs or pass statements at 16.2%; and external knowledge gaps at 8.0%, where the paper names a standard baseline or dataset without defining it. The dimension ordering numerical > algorithm > ordering > protocol holds across all twelve configurations, tracking the number of sub-decisions each claim type demands, with protocol claims the universal bottleneck. Model choice outweighs scaffold choice on average (model marginal range 0.120-0.283 against 0.193-0.249 for scaffolds), and scaffold benefit shrinks as base capability rises: the paper-to-code scaffold adds 0.116 for GPT-4o and 0.106 for Gemini-2.5-Flash but 0.029 for Claude and -0.027 for DeepSeek. Domain effects are small next to generator effects, a spread of 0.030 against a 0.219 gap between best and worst configuration. The judge agreed with human assessment on about 87% of 200 re-checked claims.

Plain-language abstract FrontierChallenge grades scientific agents on whether they finished the job, not on whether they said something plausible. Each of 97 released tasks fixes the inputs and declares a contract of required deliverables, and a task-specific executable Grader checks the whole submitted bundle. Twelve frontier models across three scaffolds completed at most 20 of the 97 tasks, while their average partial scores ran as high as 87.9 out of 100.

Motivation Existing agent benchmarks evaluate a final answer, an interaction trace, a single program, or a workflow from one discipline. Real scientific work is not shaped like that: an agent has to inspect heterogeneous inputs, choose and run an analysis, validate intermediate results, and hand back code, tables, figures, and prose that agree with each other. The authors deliberately narrow the question below autonomous science. The agent does not set the agenda or formulate the problem; it is handed a fixed objective, fixed inputs, and a stated output contract, and asked whether it can execute the workflow through to delivery.

Methodology The team collected 300 end-to-end workflows from professional analysis, computation, simulation, and research-delivery practice, screened them for representativeness, complexity, diversity, and verifiability, and packaged each as a task description, fixed inputs, a declared execution environment, an output contract, and an executable evaluation procedure, with agent-visible material separated from evaluator-side references. Tasks with purely subjective outputs or without materials for reproducible scoring were excluded. 97 tasks were released and evaluated (74 Hard, 23 Medium) across quantum chemistry, molecular dynamics, materials characterization, analytical chemistry, life science, and electrochemistry/environment, spanning 21 workflow families and requiring tools such as ORCA, CP2K, LAMMPS, AmberTools, and PLUMED; 203 remain an internal held-out set. Twelve models were run under Codex, Claude Code, and Frontier Agent. Each task's Grader returns a 0 to 100 score by checking required files, numerical results, formats, figures, code execution, and cross-artifact consistency, with rubric-defined semantic criteria delegated to a GPT-5.6 Sol judge run three times and averaged. Pass Rate counts tasks scoring at least 99.9; Avg. Score is the mean.

Results Pass Rate ranged from 3.1% to 20.6% against Avg. Scores of 67.5 to 87.9. GPT-5.6 Sol with Codex took the highest Avg. Score at 87.9 and shared the top Pass Rate of 20.6% with Grok 4.6 under Claude Code. Eight configurations scored above 80 on average and none passed more than 20.6% of tasks. Domain profiles diverge from the aggregate ranking: Grok 4.6 reached 60% Pass Rate in quantum chemistry, while analytical chemistry topped out at 4% against an 87.6 Avg. Score and electrochemistry/environment stayed at 0% against a 94.9 Avg. Score. Reported input tokens per task varied more than sixfold (2.183M to 13.730M) and mean execution time from 21.8 to 112.8 minutes. In the failure analysis, judge-assessed artifact shortfalls covered 97% of non-passing materials-characterization submissions and 43% of quantum-chemistry ones; 641 of 849 non-passing Claude Code trajectories (75.5%) ended with completion language against 90.1% of passing ones; and tool errors appeared in 94.2% of passing versus 80.7% of non-passing runs. The authors limit the claims to the released task set, the evaluated configurations, single runs, and provider-specific resource accounting.

Plain-language abstract Agent skills are prose procedure files loaded into a model's context and interpreted by a tool-calling loop, which means nothing in the runtime makes a mandated step happen. Measured against the procedures their own skills prescribe, a prose agent performs 56% of mandated steps on gpt-4o while still producing deliverables that pass output checks. SIGIL compiles a SKILL.md into an executable harness through a typed intermediate representation that marks each step as owned by code or by the model, raising step compliance to 86%, full-procedure completion from 28% to 65% of runs, and cutting median token cost to 0.58x.

Motivation Skills succeeded as an authoring format because domain experts can write, review and version them, but the property that makes them accessible leaves them unenforced. The document is consulted by the same process that is supposed to obey it, so an agent can satisfy its own reading of an instruction by writing a sentence asserting the outcome. Hand-writing a harness fixes enforcement at the cost of the authoring surface, and leaves two independent representations of one procedure free to drift. The resulting defect class is invisible to artifact-level testing: a financial-compliance report can carry reasonable figures and conclusions and still be invalid if the agent never retrieved the authoritative records, recalculated the totals, or checked the result against policy. Prior runtime supervision work adds monitors and guards that can block a disallowed action, but detection does not make a required action occur.

Methodology Compilation runs in two stages over AG-IR, a typed agentic IR whose nodes carry an owner stating whether code or the model executes the step, a modality recording how binding the source instruction was, and provenance to the mandating sentence. Extraction is the only stage containing a model and admits a rule only when a verbatim quotation supports it; six compile gates then reject an IR that points at content instead of embodying it, omits a mandated deliverable, fails to lower and type check, folds a mandatory rule into another slot's interior, or leaves a human-gated decision to model judgment. Lowering is deterministic, mapping each primitive onto an Object-Spatial Programming construct in Jac: nodes become node archetypes, edges fix walker traversal order, mandatory rules become abilities bound to node entry, model-owned nodes become typed llm() slots whose return type makes an out-of-range answer a type error, and forbidden rules lower to nothing, so the guarantee comes from the absence of a path. STRUCT-COV statically reports, per mandatory rule, whether the emitted module realizes it as a code gate, a dedicated model slot, monolithically inside another slot, or not at all, failing the last two. Evaluation covers 30 skills across document and tooling, software process, and governance and compliance families, with three process-scenario tasks per skill repeated three times per arm in isolated sandboxes, on gpt-4o and gpt-5, scored by Applicable-Mandate Compliance with a judge reading the full run and, for the harness, its node-path trace.

Results On gpt-4o the compiled harness performs 86% of mandated steps against 56% for prose, matching or exceeding prose on all 30 skills with 28 strict wins, 2 ties and no losses, and completing the full applicable procedure in 65% of runs against 28%, a factor of 2.3. Moving to gpt-5 leaves the harness at 86% while prose rises to 68%, so the advantage narrows from 30 points to 17; the harness artifact is byte-identical across both sweeps, which is what makes the guarantee model-independent by construction. Median token cost is 0.58x prose, cheaper on 24 skills and as low as 0.02x on a nearly all-code skill, with the exceptions concentrated in skills organized around a genuine tool-using loop, reaching 7.64x on using-superpowers and 3.09x on systematic-debugging, where the prose agent was cheaper because it truncated or skipped the loop. The compiler realizes 37% of mandates as code-owned gates on average, 32% to 44% by family, and the four skills where the harness loses on gpt-5 are judgment-heavy ones with little to compile.

Plain-language abstract Real maintenance is a stream of related fixes on a codebase you yourself just changed. Every SWE benchmark instead resets the repository, hands over one self-contained issue, and grades it in isolation. ChainSWE keeps the repository, orders real issues chronologically within a project, and asks whether an agent's earlier patches leave a usable starting point for the later ones. Performance drops by up to 70% as chains get longer, and roughly half the downstream failures are caused by the agent's own accumulated edits rather than by the bug in front of it.

Motivation Agent performance has improved rapidly across SWE-bench, SWE-bench Live, SWE-rebench, SWE-Gym and SWE-bench Pro, but all of them share one protocol: a fresh container reset to a clean base commit, one problem statement, a fresh conversation, and grading against pre-written tests from that issue. This measures single-shot issue resolution and deliberately removes the cross-task dependencies that characterize real maintenance. It says nothing about whether an agent avoids unnecessary edits, resolves latent multi-file dependencies, or manages context across an evolving sequence of related fixes. In practice an engineer must leave the codebase both correct for the current issue and usable as the starting point for future work, reading surrounding context and adapting to the repository state they inherit. Adjacent sequential benchmarks (AgentBench, AgentBoard, WebArena, OSWorld) and long-conversation memory benchmarks are sequential but reset between tasks or track dialogue state rather than persistent changes to an external artifact.

Methodology Instances are pooled from six repository-level SWE benchmarks, all Python with pre-built Docker images for reproducible test execution. Per repository, instances are sorted by commit date and grouped by a sliding window into chains when they overlap in the code they touch, then validated by containerized re-execution: replay the accumulated gold patches, run the bug's test commands, and require that all FAIL_TO_PASS tests pass with no PASS_TO_PASS regression. A chain is accepted only if every filter stage clears. Length-2 chains are dropped during data selection. At evaluation step k the agent receives only the k-th issue statement and works on the repository state produced by the previous steps, with the Docker image reset only to the base commit of the first bug in the chain. Scoring is both per-bug, by chain position, and full-chain, where a chain counts as successful only if every bug in it is resolved, alongside average API cost per task and per chain. Seven state-of-the-art models are evaluated on a fixed SWE-EDIT scaffold under three context-management configurations. Failures at a downstream position that are attributable to accumulated agent-generated state rather than the intrinsic difficulty of the current bug are labeled chain errors.

Results The dataset is 100 chains, 304 instances, 54 repositories, with chain lengths from 3 to 5 after selection. Performance falls by up to 70% relative to the single-issue setting, and the decline is steepest at the deepest chain positions. Chain errors account for 318 of the 663 downstream BASELINE failures at positions 2 and 3, 48% overall, growing with depth from 43% at position 2 to 52% at position 3. On context management, conversation memory across bugs yields only a marginal gain and only for GPT-5.5, while summarization and sub-agent delegation both consistently degrade performance. The two named failure mechanisms are illustrated by concrete chains: amaranth for overshoot, where three unrelated backend files rewritten during an earlier fix cause all eight downstream tests to fail, and MONAI for undershoot, where omitting three supporting refactors from a five-file gold patch breaks a downstream test despite a correct modification to the target file. The authors read the results as pointing at dependency tracking, long-horizon reasoning and repository-state management in agent harnesses rather than at further gains in isolated issue resolution.

Proposes using LLMs to reduce the cost that keeps verification-aware languages out of ordinary practice.

Why it matters States the adoption thesis this whole area rests on, so it is worth reading as a claim to be tested.

A roadmap for fusing LLMs with formal methods toward trustworthy AI agents.

Why it matters Useful as an agenda, and useful for seeing which of its proposed steps have since been attempted.

Experimental study of whether LLMs help students prove software correctness in Dafny.

Why it matters Learnability data, which decides adoption more than raw capability does.

Investigates failure modes when probabilistic models produce formal specifications that deterministic verification then trusts.

Why it matters The epistemological problem underneath every pipeline here, studied rather than asserted.

Examines failure prevention in AI-driven software engineering and where autonomy should stop.

Why it matters Argues the control question directly instead of assuming more autonomy is the goal.

Formal specification and runtime enforcement of behavioral contracts for autonomous agents.

Why it matters Points the tooling at the agent itself rather than at the code it produces.

Surveys autonomous research agents and names verification as the unclosed gap.

Why it matters The same specification gap seen from the science-automation side, which shows it is not a software-engineering quirk.

Certifies the results of a verification tool by mirroring them into a foundational setting (Foundational VeriFast).

Why it matters Who verifies the verifier, answered pragmatically. The trusted base matters more once proofs are machine-written.

Frames the gap between informal intent and precise program behavior as the grand challenge for reliable coding with agents.

Why it matters The best single statement of why this explorer exists. The bottleneck moved from writing code to saying what the code should do.

A research vision for the next generation of formal methods built around learning, from contract synthesis to formal semantics.

Why it matters Sets out what a formal-methods agenda looks like when learned components are assumed rather than resisted.

Gives a mechanically checkable capability-containment argument for agent skill manifests.

Why it matters The strongest current attempt at proving something about what an agent is allowed to do.

Applies formal reasoning to a mature industrial C++ codebase rather than to a designed-for-verification system.

Why it matters Most formal methods case studies start at design time; this is the retrofit case almost everyone actually faces.

Plain-language abstract Coding agents are usually improved by giving them better tools, skills and workflows. Tian's argument is that the input is the weaker link: task descriptions are ambiguous, incomplete or missing context, so even a strong model is inferring intent from an unreliable statement of it. WiseSpec builds the requirement instead of consuming the prompt, scores that requirement by generating code and tests from it and running them, and refines it until the score stops improving. On three SWE-bench variants and two models it beats Agentless, Trae-agent and Claude Code on both syntactic and functional correctness.

Motivation Work on repository-level code generation has concentrated on how a model solves a task rather than on the quality of what it is asked to solve. Most methods consume the original problem description directly, which assumes that description faithfully specifies intended behavior. The paper's position is that this assumption does not hold in practice: descriptions are frequently ambiguous, incomplete or missing critical context, and deficient requirements propagate errors downstream into the implementation. Requirements engineering already treats specification quality as a first-class step, but its usual difficulty applies here too, since requirements written in structured natural language carry no formal semantics and cannot be evaluated directly or quantitatively.

Methodology WiseSpec has three components. Requirement generation simulates program comprehension: starting from the task description it iteratively collects code snippets from the target codebase, expanding retrieval along program dependencies and using what it has already gathered to guide the next step, then organizes the fragments through a requirement DSL of nine primary attributes and seventeen sub-attributes covering both architectural and fine-grained implementation detail. Requirement quality assessment reformulates the scoring problem as execution-based code evaluation: generate executable code and tests from the requirement, run them, and treat execution correctness as a proxy for requirement quality, with a strict criterion that the code is accepted only if it passes all generated tests. Requirement refinement diagnoses failures into three mutually exclusive categories, Conflict, Omission and Ambiguity, applies predefined alignment rules to produce actionable feedback, re-assesses, keeps the highest-scoring candidate at each iteration under a greedy strategy, and records feedback that failed to improve the score as counterexamples for later iterations. Evaluation compares against Agentless, Trae-agent and Claude Code on 100 randomly sampled instances each from SWE-bench-Lite, SWE-bench-Verified and SWE-bench-Pro, using DeepSeek-V3.2 and Qwen-Plus-2025-12-01, scored on %Applied (the patch applies) and %Resolved (it passes the gold tests).

Results WiseSpec was best in all six settings of three benchmarks by two models, improving %Resolved by 2 to 29 points and %Applied by 11 to 63 points over the baselines, with a Wilcoxon signed-rank test at alpha 0.05 giving p below 2.5e-4 for both metrics. The %Applied gains are the largest: WiseSpec reached 100%, 93% and 100% with DeepSeek and 100%, 98% and 99% with Qwen, against 72%, 77% and 84% for Claude Code with DeepSeek. On functional correctness the margins are narrower, for instance 39% against 36% on SWE-bench-Lite with DeepSeek, and widest on the hardest benchmark, 35% against 24% on SWE-bench-Pro. A check on a stronger model narrows it further: on SWE-bench-Pro with Claude-Opus-4.8, Claude Code scored 53% and WiseSpec 56%. The reported average improvement in %Resolved is 13.17%.