Specification generation and quality

(authored by agents unless marked 🧑)

• 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers: An LLM writes a short checkable 3D DSL instead of C, EverParse compiles it to verified C, and the parser proof is reused rather than generated per protocol.
• A Specification Logic for Programs in the Probabilistic Guarded Command Language (Extended Version): Defines probabilistic dynamic logic for pGCL programs as a specification language; the proof system it aims at is future work, not delivered.
• A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs: Preguss has an LLM write ACSL contracts and loop annotations until Frama-C/WP proves every analyzer-reported runtime error impossible, so each alarm becomes the verification goal.
• Practical Range Refinement Types with Inference: Range refinement types are inferred by backward dataflow, and a forward checker validates each candidate, so an unsound guess is harmless; the Verus analogue is candidate invariants checked by the proof checker.
• LLM Assisted Coding with Metamorphic Specification Mutation Agent: CodeMetaAgent uses metamorphic relations inside the generation loop to mutate specs and tests, improving consistency; it diversifies tests rather than formally verifying code.
• The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification: CAISAR lets users write high-level ML model properties in Why3 and dispatches them to several robustness verifiers, narrowing the spec-to-check embedding gap.
• Hermes: Unlocking Security Analysis of Cellular Network Protocols by Synthesizing Finite State Machines from Natural Language Specifications: Synthesizes communicating FSMs from 4G/5G natural-language standards, model-checks them, and finds 3 new vulnerabilities; extraction reaches 81-87% accuracy against gold FSMs.
• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement: A verifier only guarantees that code meets the supplied spec, and assume(false) passes Verus, so the spec and its critique remain the trusted part.
• Specifying a Realistic File System: AFS specifies a flash file system as a nondeterministic monad whose choice is a union of outcomes; the Verus analogue is a ghost spec function returning the set of allowed outcomes.
• Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code: Makes the module interface a checked artifact (entry functions, entry order, permitted external calls), motivated by untrusted subcontractor or LLM code; 6 principles become 17 rules.
• Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving: A checked proof certifies only the formal statement the kernel received, and benchmark formalization faults such as omitted hypotheses are a larger risk than proof errors.
• An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications: LLM repair of faulty Alloy specs was checked by the Alloy Analyzer, and a dual-agent variant turns analyzer reports into at most two sentences of repair advice.
• An Empirical Study of LLM-Generated Specifications for VeriFast: LLM-written VeriFast auxiliary specs preserve behavior in over 91% of outputs but verify only 31.4% (855 of 2,727), with Gemini 2.5 Pro best at 39.7%.
• ANCORA: Learning to Question via Manifold-Anchored Self-Play: One policy plays spec proposer and implementer, rewarded only by the Verus verdict; sparse valid outputs collapse plain RL, and iterative SFT on verified rollouts lifts Dafny2Verus pass@1 from 0.4% to 26.6%.
• Weakening Goals in Logical Specifications: Counterexample-guided weakening finds a property between the desired and critical specs when a change breaks verification; demonstrated on propositional logic only.
• LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation: GPT-4o generates SoC security properties and SVAs refined by JasperGold feedback and a vacuity screen, but the paper reports no classification error rate and no RAG ablation.
• Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph: Aria auto-formalizes math statements into Lean and counts success only if they compile and pass semantic approval, so faithfulness of the statement is the bottleneck.
• Assured Automatic Programming via Large Language Models: Program-proof co-evolution repairs (code, spec, test) tuples from one NL intent, splitting facts into hard and soft intent, with the verifier checking every candidate.
• Autoformalization with Large Language Models: Codex autoformalizes 25.3% of sampled competition math perfectly, and missing relevant prompt examples made it invent nonexistent syntax.
• Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles: An LLM adds Dafny annotations to unchanged code and verifies 108 of 110 tasks, with static test asserts as spec oracles, but the result shows Dafny satisfaction, not requirement completeness.
• SpecPylot: Python Specification Generation with Large Language Models: An LLM writes icontract specs and CrossHair checks them; only a REFUTED result with a concrete counterexample drives refinement, and PASSED is not a proof.
• From Helpful to Trustworthy: LLM Agents for Pair Programming: Preliminary AutoReSpec (72 programs) and AutoJML (120 programs) results; trust should come from external evidence, with the developer confirming the spec matches intent.
• AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL: Builds a knowledge graph from a hardware spec and parsed RTL, then has an LLM write SystemVerilog assertions that Cadence Jasper checks.
• VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation: Adversarial test expansion shows sparse tests overestimate LLM verifiable code generation: on Verina Plus, gpt-5.5’s code score falls from 96.83 to 86.24 and its spec score from 68.78 to 44.44.
• Improving Dynamic Specification Inference with LLM-Generated Counterexamples: LLM-written counterexample tests attack dynamically inferred Java postconditions, raising precision from 67.83% to 74.17% while recall stays at 54.57%.
• Fulminate: Testing CN Separation-Logic Specifications in C: Syntactic restrictions that make CN separation-logic specs provable also make them executable, so one spec serves both runtime testing and static proof.
• LLMs as verification oracles for Solidity: GPT-5 classifies natural-language Solidity properties with 92% accuracy and F1 on 667 tasks, with no unknown answers and counterexample transactions for bugs.
• Working Document - Formalising Software Requirements with Large Language Models: A verified contract proves only the requirement as encoded, so a human must confirm the contract matches intent, and a review of 94 papers catalogs the field.
• Leveraging LLMs for Formal Software Requirements: Challenges and Prospects: Small, well-scoped assertions verify more reliably than full contracts, so an LLM should first generate small ensures or assert clauses and let verifier feedback drive refinement.
• Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?: LLMs can infer preconditions as well as postconditions from docstrings, since postcondition-only specs admit invalid inputs and cause false alarms.
• Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation: Open-weight LLMs rarely write TLA+ that passes TLC; the best open strategy passes only 8.6% of runs, and few-shot wins mainly on parsing.
• TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation: Execution-grounded TLA+ benchmark: a mutation probe replacing the safety invariant with TRUE shows many TLC-passing outputs are not substantive, so pass rates overcount.
• Formalizing and validating properties in Asmeta with Large Language Models (Extended Abstract): A feasibility demo shows an LLM can help turn informal requirements into Asmeta temporal properties checked via NuSMV; there is no integrated system or evaluation.
• Automated Repair of Unrealisable LTL Specifications Guided by Model Counting: AuRUS repairs unrealisable LTL assume-guarantee specs by changing assumptions and guarantees, scored by similarity; it repaired all benchmark specs.
• Natural Language to First-Order Logic LLM-based Autoformalization: Ontology quality for NL-to-FOL autoformalization is unmeasured, and one sentence admits several formulas with different commitments, so intended meanings must be fixed before judging faithfulness.
• Towards Trace-based Deductive Verification (Tech Report): Trace contracts specify events and intermediate states that pre/postconditions cannot, with a soundness-proved symbolic-execution calculus for recursive procedures.
• From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs: Full proof generation from NL requirements reached 7.7% pass@1, while proof completion reached 18.3%, so partial-artifact tasks are easier than whole ones.
• Deductive Verification of Smart Contracts with Dafny: Carry a global invariant in every method’s requires and ensures so the verifier checks it across any call sequence; no Dafny-to-EVM compiler exists, so the EVM step is assumed.
• Mitigating hallucinations and omissions in LLMs for invertible problems: An application to hardware logic design automation: Round-trip check: a human spec is encoded to Verilog by one LLM, decoded back by a different LLM, and compared, which exposes forward, inverse, or spec errors but cannot catch matching wrong specs.
• FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs: C++ specification dataset made by LLM-translating verified Dafny programs to C++; testing and partial review do not establish semantic equivalence.
• BODHI: Precise OS Kernel Specification Inference: A 519-line C-to-Python translation guide lifts Pass@1 by 11.0 to 31.8 points across nine models for LLM kernel-spec inference, though results come from one greedy run.
• SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop: SpecLoop writes RTL to prose spec, reconstructs RTL, and checks equivalence with Yosys EQY to bounded depth; a pass shows the spec is detailed enough, not complete or faithful.
• NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models: Replacing concrete atomic propositions with placeholders lets an NL-to-STL model learn only logical structure, which transfers across domains with about 95-97% atomic-proposition accuracy.
• Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models: Trusta checks assurance cases with Z3 and MONA; machine-generated cases match human ones at only 50-80% similarity.
• Enhancing LLM-based Specification Generation via Program Slicing and Logical Deletion: Generating ACSL specs per program slice, and deleting failing clauses before whole-function verification, avoids discarding correct clauses whose preconditions are not yet generated.
• Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation: Repairing LLM-written ACSL specs from verifier diagnostics yields more verified programs but costs more runtime, tested on 49 Frama-C programs across six models.
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation: CodeSpecBench tests LLM-written executable pre/postconditions on 2,494 LeetCode tasks and 500 SWE-bench issues, scored by valid/invalid inputs and trigger/regression tests.
• Judging Is Not Enumerating: Silent Omissions in LLM-Authored Acceptable Sets: When LLMs author an acceptable set rather than judge candidates, they mostly omit members, and the omissions resist audit.
• Can Large Language Models Model Programs Formally?: TLC runnability and state similarity can score LLM-written TLA+ models of Python programs, but the oracle models are not proven to match their source programs.
• Prove2Me: An Open Collaborative Platform for Scaling Math Formalization: The kernel certifies a proof of the stated statement, not that the statement is faithful; Prove2Me audits only headline goals, definitions, and milestone lemmas via blind read-back.
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization: Autoformalization is rewarded for a critique step only when the critique finds real semantic gaps, because compiling Lean statements alone allows unfaithful specs.
• SpecFirst: Behavioral Specification Elicitation as a First-Class Step in Agent-Based Program Synthesis from Scratch: Having an agent probe a black-box binary and write a behavioral spec file before coding raised test pass rates by 6.9 to 21.3% relative across four models on ProgramBench.
• ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification: An agent asks users to clarify vague and ambiguous requirements before translating to STL, and its ambiguity detector reaches 91.0% F1.
• Passing Proofs That Prove Nothing: Deciding Postcondition Vacuity, Precondition Satisfiability, and Contract Completeness for Rust and Kani: A passing Kani proof can constrain nothing; postcondition vacuity is decided by havocing one arbitrary return value, and the check is mechanized in 20 Lean theorems.
• Clover: Closed-Loop Verifiable Code Generation: Clover accepts a code, annotation, and docstring triple only if six pairwise checks pass, including regenerating code from the annotations to catch trivially weak specs.
• Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis: Split code into formal reactive synthesis for control and LLM-filled data terms, which reaches 61.5% at 10 conditions where LLM-only reaches 0%, but the user must still check the spec.
• Combining Mechanical and Agentic Specification Inference for Move: For Move specs, the agent should propose loop invariants before weakest-precondition runs, since weakest-precondition output first gave vacuous specs that misled the model.
• Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study: A successful build does not show the verification task was preserved, so LLM-proposed proof edits need protection of statements and definitions, not only a passing build.
• FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation: Silent correction: an autoformalizer can turn x in R into x in N, making a false conclusion provable, so each formal step is tested with a perturbed invalid twin.
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models: Translating natural language to temporal logic as user-editable fragment pairs lets users fix ambiguity locally, instead of rewriting the whole formula.
• Local refinement typing: Fusion infers SMT-checked intermediate refinement types from exported signatures, reducing the annotations a programmer must write.
• Towards Formal Verification of LLM-Generated Code from Natural Language Prompts: The verifier checks the LLM output against a user-reviewed formal query, and only the human can decide whether that query matches intent.
• Can LLMs help find Ambiguities in Protocol Specifications?: An LLM reads protocol prose for ambiguity while a deterministic scaffold supplies coverage, using communicating finite state machines to define gaps and forks.
• Contract Strengthening through Constrained Horn Clause Verification: Strengthen valid contracts with a CHC-based analysis so callers verify; Stainless times out on rev with the weak contracts and proves both after strengthening.
• Reducing the Number of Annotations in a Verification-oriented Imperative Language: Pest is a verification-oriented language designed so programs verify more easily; students verified sorting and search with it, qualitatively, with no benchmark.
• A framework for assessing the capabilities of code generation of constraint domain-specific languages with large language models: For OCL and Alloy generation, validate in stages so syntax is separated from semantics, since prompt-template comparisons were inconclusive.
• Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler: Djinnlang requires constraints to determine the output uniquely, so the LLM must prove the relation is deterministic, not merely satisfiable.
• Proving the Coding Interview: A Benchmark for Formally Verified Code Generation: Lean theorem statements are filtered by unit tests and Plausible property testing, but these are filters, not proof that the statements are the intended specs.
• FVSpec: Real-World Property-Based Tests as Lean Challenges: Mining 7,413 property-based tests from 497 repos yields 2,623 Lean specs, but these tests may omit preconditions or encode bugs, so they are not ground truth.
• Predicate Subtypes in VerCors: VerCors rewrites predicate subtypes such as NonNull and Index(len) into ordinary contracts, but strict arithmetic checks can fail on intermediate subexpressions like (x-2)+2.
• ModelForge: Using GenAI to Improve the Development of Security Protocols: ModelForge uses a fine-tuned LLM to translate natural-language protocol specs into CPSA input, so the CPSA model finder supplies the checking step.
• Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification: AutoSpec has an LLM synthesize ACSL specs bottom-up over a call and loop graph, with Frama-C WP checking each round, and reports 199 of 251 tasks solved, but only for C.
• Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?: GPT-4 writes postconditions from NL; plain true is correct but scores 0 on bug-completeness, so judge specs by how many mutants they reject, not by passing tests alone.
• Fidelity Probes for Specification-Code Alignment: An LLM answers behavior probes from the spec alone, compared with answers derived from code; disagreements split into contradictions and coverage gaps.
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages: Test-as-Hoare-triple scores LLM postconditions, but it passes a vacuous ensures true, so completeness needs output mutation as a second metric.
• Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench: Executable model specs can pass syntax, bounded exploration, and invariant checks, yet replay only 21.4% to 89.3% of real spinlock trace windows, so trace conformance is the stronger test.
• Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization: Meaning-preserving rewording changes autoformalizer output: frontier surface consistency is 19-50% on ProofNet#, and some rewrites change meaning, so rewrite rules need meaning-preservation references.
• Scenic: a language for scenario specification and scene generation: Scenic is a probabilistic language for scenario specification that generates test sets and emphasizes hard cases for perception systems.
• Agentic Specification Generator for Move Programs: Per-clause-class LLM agents with Move Prover feedback produced 300 of 357 verifiable specs, but 33% of generated clauses were absent from expert specs.
• Fyan: A Human–AI Harness with Semantic Auditing for Document-Level Formalization: Fyan pairs slots of informal and formal statements and scores unpaired source slots as omissions, because a proof assistant checks the theorem, not its fidelity to the source.
• Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks: Estimates a PCFG over many sampled SMT-LIB outputs; structural uncertainty decides when to accept, abstain, or review an LLM-generated artifact.
• Herald: A Natural Language Annotated Lean 4 Dataset: Herald extracts theorem structure from Mathlib, generates NL-FL pairs, and validates them with the Lean compiler plus back-translation and NLI checks.
• IronSpec: Increasing the Reliability of Formal Specifications: A passing proof can hide a wrong spec, so an automatic sanity checker flags unconstrained inputs and outputs, and mutation testing tests the spec independently of the implementation.
• Natural Language Specifications in Proof Assistants: A prototype parses a fragment of English into Coq propositions, letting a user write a natural-language spec as a proof goal.
• Trustworthy Formal Natural Language Specifications: A categorial grammar in Lean 4 parses natural-language requirements into terms with inspectable certificates, guarding against mistranslated formal claims.
• Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods: Frama-C analysis output shapes LLM ACSL contracts: path examples give abstract postconditions, while EVA alarms give range preconditions that may just suppress alarms.
• Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis: Feeding Frama-C symbolic outputs (PathCrawler, EVA) into DeepSeek-R1 prompts steers ACSL function-contract synthesis, a neuro-symbolic spec method.
• ObSynth: An Interactive Synthesis System for Generating Object Models from Natural Language Specifications: ObSynth turns a natural-language app description into an editable object model via few-shot GPT-3 prompts, keeping a human in the editing loop.
• An Evaluation Benchmark for Autoformalization in Lean4: 101 formal/informal mathlib4 theorem pairs measure how GPT-3.5, GPT-4, and Gemini Pro autoformalize statements into Lean 4.
• Autoformalizer with Tool Feedback: Autoformalizer with tool feedback runs a Lean syntax check first, then an LLM consistency judge ensemble; the judges ignore the proof, so a compiling and judged-consistent statement can still be wrong.
• EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations: EquivSVA organizes assertion data by behavior family, with four equivalent RTL implementations each, to test whether generated SVA express behavior rather than one RTL.
• Formal Specifications from Natural Language: A fine-tuned LM translates English into regex, FOL, and LTL, beating prior regex SOTA by 6 points; outputs are checked by comparison, not proven.
• Neurosymbolic Auditing of Natural-Language Software Requirements: Formalizing NL requirements into one SMT model yields consistency, vacuity, violatability, and redundancy checks, which are review signals, not verdicts on the requirements.
• Automated Repair of Declarative Software Specifications in the Era of Large Language Models: One-shot ChatGPT repair of Alloy specs with no verifier feedback trails ARepair, ICEBAR, BeAFix, and ATR overall but fixes bugs no other tool fixes, and fix comments matter most.
• A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs: Heapster extracts a pure functional spec from memory-safe C via permission types the user writes per function; loops need reachability hints, and array bounds checks become possible-error terms in the spec.
• Beyond Code Generation: Assessing Code LLM Maturity with Postconditions: Postcondition generation on EvalPlus separates same failures from semantic equivalence, and metric denominators must stay separate: problems for some metrics, mutants for others.
• CASP: An Evaluation Dataset for Formal Verification of C Code: CASP offers 506 Frama-C-verified C-plus-ACSL pairs for spec-to-code evaluation, and regex mining only finds candidates; it cannot show a spec is valid.
• Sage: Formalization with Semantic Correction: Autoformalization must separate assertions from open questions, since encoding a question as a claim or an existential changes what the prover is asked to do.
• Stratified Consistency Distillation for Natural Language Formalization: Sampling translations, clustering them by Z3 equivalence, and training only on pseudo-labels chosen by semantic entropy distills a frontier NL-to-SMT translator into a 7B model.
• SecGoal: A Benchmark for Extracting Formalizable Security Goals from Protocol Documents: A benchmark of 391 security-goal statements and 131 formal properties from 15 protocol documents; the task is specification extraction, not proof.
• Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language: Relaxed NFL keeps natural math notation, elaborates it to Core NFL, and generates verification conditions; the evaluation measures only generation, not proof discharge.
• Automatic Assertion Mining in Assertion-Based Verification: Techniques, Challenges, and Future Directions: A survey of hardware assertion miners warns they overgenerate, duplicate, conflict, and miss corner cases, so mined assertions must still be checked.
• Spec2Vision: Contract-Guided Delivery of AI-Generated Computer Vision Pipelines: Explicit CV task contracts with bounded repair reach 81/85 strict deliveries; removing compatibility scaffolding drops this to 58/85.
• Automated formalisation of informal specifications by combining LLMs and grammar-based language processing: An LLM rewrites Java requirements into grammar-compatible sentences, raising JML derivation coverage from 23% for grammar alone to over 90% of sentences.
• Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving: CEGIS with an LLM learner and Z3 verifier, shown only on block-world planning; the paper has no theorems and no other experiment.
• Multilingual Mathematical Autoformalization: Back-translating formal libraries into informal text and training on reversed pairs yields an autoformalizer, though only 16 to 18% of joint-model outputs were acceptable to two raters after minor correction.
• Limits to Verification and Validation of Agentic Behavior: Defines a deontology as a set of Good histories and requires viability: after any Good history, some action keeps it Good.
• Can Large Language Models Autoformalize Kinematics?: An LLM formalizes kinematics problems for KeYmaera X through a parser-feedback repair loop capped at three repairs, and the cap is not shown sufficient.
• PolicyKG: An Agentic LLM Pipeline for Translating Institutional Policies into SHACL Knowledge Graphs: Agentic LLM stages extract policy text, classify deontic rules, formalize FOL, and deterministically emit SHACL-validated knowledge graphs under a fixed stage order.
• An iterative approach to precondition inference using constrained Horn clauses: Infers weak safe preconditions for CHC programs by iterating partial evaluation, constraint specialization, and trace elimination; the weakest safe precondition is not computable.
• Precondition Inference via Partitioning of Initial States: Sufficient preconditions come from partitioning initial states, and the result is correct only relative to modeled exceptions, so unmodeled overflow stays outside it.
• Unifying Inference-Time Planning Language Generation: An LLM writes PDDL checked by a planner and VAL, where one extra intermediate representation beats direct planning in 8 of 8 cases and natural-language intermediates hurt.
• KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification: KaPilot derives Kani contract requirements from Rust docs with the implementation hidden, using atomic traceable requirement sentences as the spec target for memory safety and panic freedom.
• KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base: KBSpec generates JML specs with a memory that grows from verifier feedback and no weight updates, and repair-derived items dominate the memory.
• Generating Logical Specifications from Requirements Models for Deduction-based Formal Verification: Generates temporal-logic specs from UML requirements models for deductive checking; steps 1-3 are engineer-authored, so automation is partial.
• Instructions Unclear: Undefined Behaviour in Cellular Network Specifications: Writing a protocol spec in TLA+ forces explicit handling of undefined inputs, which natural-language specs leave unstated.
• On Integrating Deductive Synthesis and Verification Systems: Synthesizing programs from relational postconditions works, but weak specs give useless programs, such as a split that returns (lst, Nil), so spec strength decides output quality.
• Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Engineering: A proof of program P against requirements R under model M cannot guarantee stakeholder acceptance, since intent-to-requirement and world-to-model gaps stay outside the inner loop.
• The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems: Synthesized implementations are correct only relative to the spec, and the resulting transducer can be hard to understand.
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents: Intent formalization exposes ambiguity by writing an executable postcondition before trusting generated code, and LLM-written postconditions caught 1 in 8 real Defects4J bugs.
• Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection: NL2FOL chains LLM steps to turn arguments into FOL and asks CVC4 for validity or a counterexample; GPT-4o reaches 0.78 F1 on LOGIC.
• Survey of annotation generators for deductive verifiers: Survey of Java spec generators: Daikon emits 158 annotations with 53% wrong, GPT-4 emits 42 with 6 wrong, and the best tool still invents a precondition, so generated specs need human review.
• Shape Analysis via Second-Order Bi-Abduction: S2 synthesizes per-method heap predicates via second-order bi-abduction and derives definitions from relational assumptions.
• SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic: SLING infers heap invariants from debugger traces, and the paper states it gives no correctness guarantee beyond the observed traces.
• SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference: Postcondition inference should separate probes from submissions and score by correctness and mutant rejection, since a trivial True postcondition passes tests yet rejects no mutants.
• Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics: Research vision for contract synthesis from natural language, specification reuse by graph matching, and UTP semantics; the VERIFYAI architecture is conceptual, not evaluated.
• Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference: On 700 Java programs (6,219 variants), LLMs write JML specs for simple control flow but struggle with loops.
• Lean-GAP: A Dataset of Formalized Graduate Algebra Problems: Elaboration is necessary but not sufficient: a Lean statement can compile yet be mathematically vacuous, so meaning checks by humans are the bottleneck.
• LeetProof: certified synthesis with a multi-modal verifier: LeetProof checks LLM-written specs by testing about 10 I/O examples and type-directed mutations before proving, since implication instead of equivalence admits false and mutation exposes it.
• Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework: AutoSafeLTL: an LLM generates LTL, and a candidate is accepted only if its Buchi language is included in every safety constraint’s language.
• Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling: Protocol specs can route human review to fields with weak evidence, failed cross-checks, and high impact, since the reviewed intermediate representation, not raw LLM output, is the trusted source.
• Correct Tests Are Not Enough: Measuring and Training Oracle Conversion in Specification-Based Test Generation: Spec-based test generation loses kills when generated outputs are wrong, so measure effective kill rate separately from potential kill rate.
• Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning: L4L turns statutes and cases into typed constraints checked by Z3, then lets a judge LLM render verdicts, keeping applicability checks symbolic.
• Verifying Consistency and Validity of Formal Specifications by Testing: Tests a formal spec before implementation: consistency and validity are checked by evaluating derived proof obligations on selected input/output bindings.
• ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity: ASSESS grades statement similarity via tree edit distance over Lean operator trees; a nonzero score is triage, not proof of equality, and the metric penalizes equivalent reorderings.
• CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization: A critic LLM checks whether compiling Lean code means what the problem asked, reaching 87-89% on compilable-but-wrong pairs, since a proof of an under-specified contract is still a valid proof.
• Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees: DSR splits a Lean statement into components, builds an operator tree, and repairs compiler errors at the smallest subtree that explains them; evaluated on 156 theorems.
• Can Formal Specifications Be Synthesized from Tests Alone?: JML contracts inferred from tests and execution traces, never source, succeed for 11 of 22 APIs, and traces expose state changes that tests never assert.
• Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification: Across 13 models, Dafny specification generation for multi-function programs is 95.67% syntactically correct but only 3.69% verified at Pass@8.
• FormalAlign: Automated Alignment Evaluation for Autoformalization: A fine-tuned Mistral-7B scores informal-formal alignment with a contrastive loss and catches dropped variables that Lean accepts, such as 80c=63 for 63a=80*c.
• Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision: Three-agent pipeline uses formal specs to bridge natural-language requirements to code; a vision with no quantitative evaluation.
• Array-Carrying Symbolic Execution for Function Contract Generation: Symbolic execution synthesizes ACSL requires, ensures, and assigns for C, and success means Frama-C WP proves every generated goal.
• FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization: Evolutionary search keeps many compiling autoformalization candidates and tests each under a fixed proving budget, so compiling but wrong candidates serve as stepping stones.
• NL2SpaTiaL: Generating Geometric Spatio-Temporal Logic Specifications from Natural Language for Manipulation Tasks: Predicting a semantic logic tree and rendering syntax deterministically yields more accurate, sample-efficient spatio-temporal logic specs than emitting a flat logic string.
• Beyond Objective Equivalence: Constraint Injection for LLM-Based Optimization Modeling on Vehicle Routing Problems: Matching objective values misses wrong constraints; a constraint-injection verifier adds feasibility tests on labelled solutions to catch both over- and under-constrained models.
• SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications: SpecEval tests LLM spec comprehension on 204 Java programs through judgement, selection, infilling, and generation; distractors include weak but valid specs that a good model must reject.
• From One Thousand Pages of Specification to Unveiling Hidden Bugs: Large Language Model Assisted Fuzzing of Matter IoT Devices: Queries GPT-4-Turbo at temperature 0, cluster by cluster, to extract device data types and commands from the Matter specification, then fuzzes IoT devices with them.
• Bridging Natural Language and Formal Specification–Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs: Zero-shot GPT-4o got 49 of 112 aerospace requirements right while atomic-proposition recall was 98.5%, so the failure is structure, not vocabulary.
• Automated LTL Specification Generation from Industrial Aerospace Requirements: Industrial requirements go through templated natural language to LTL with domain grounding, since without grounding LLMs invent atoms or drop cycle semantics.
• Reversa: A Reverse Documentation Engineering Framework for Converting Legacy Software into Operational Specifications for AI Agents: Multi-agent pipeline recovers traceable operational specs and explicit gaps from legacy code for use by coding agents.
• MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs: An LLM translates programs to Dafny and proves safety against a frozen spec library, certifying 220 of 220 programs, but the certificate covers the Dafny translation, not the original program.
• Spectra: a specification language for reactive systems: Spectra separates environment inputs from system outputs and assumptions from guarantees, translating every well-formed specification to GR(1) synthesis.
• From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation: An SVA-generating agent that retrieves only relevant RTL fragments and runs a vacuity check raised functionality from 43.2% to 82.0%, though its figures are assertion-level aggregates, not design pass rates.
• Autoformalization of Game Descriptions using Large Language Models: One-shot prompting plus solver syntax feedback turns game descriptions into executable Prolog; the paper’s dataset count is inconsistent (105 vs 110).
• Capturing System Designs with Formal Executable Specifications: Argues for executable formal specifications from early design; its evidence is mostly retrospective, such as spoofing flaws in IE and bugs in C semantics.
• Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases: Theory-level autoformalization builds whole formal libraries (axioms, definitions, lemmas) instead of translating one theorem against a library.
• Towards AI-Assisted Synthesis of Verified Dafny Methods: GPT-4 Dafny methods verify at 64.04% verify@5 on 178 MBPP tasks, but verified is not correct, since manual review finds strong specs for only 103 of 178 (58%).
• The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements: Bidirectional provability fingerprinting detects drift between NL and Lean statements (forward and backward probes), reaching F1 0.91 and 0.896 detection at 3% false positives.
• EvoSpex: An Evolutionary Algorithm for Learning Postconditions: Postconditions inferred from bounded executions by genetic search describe likely current behavior, not guaranteed truth, since a mutant rejected as invalid may be a valid execution.
• Fuzzing Class Specifications: SpecFuzzer ranks likely Java class specs from grammar fuzzing, Daikon filtering, and mutation clustering, but its output is a likely spec, not a proof.
• Autoformalization of Agent Instructions into Policy-as-Code: A grounding layer generates the Cedar schema from MCP tool definitions, and hard checks use Cedar tooling; the LLM soft judge sits outside the formal trust boundary.
• A Pilot Benchmark for NL-to-FOL Translation in Planetary Exploration: A pilot benchmark translates planetary mission descriptions into first-order logic with controllable schema knowledge.
• LLM-Based Test Oracles: Source-of-Authority Taxonomy—A Systematic Literature Review: LLM test oracles should be classified by source of authority, since a model-synthesized relation counts as a spec only when it is an inspectable artifact.
• Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control: The LLM writes only the control logic of TSL specs, with data operations hidden behind function and predicate signatures in the prompt, which separates data from control for reactive synthesis.
• MutDafny: A Mutation-Based Approach to Assess Dafny Specifications: Mutants that still verify flag possibly weak specs; a 284-survivor audit found 27.1% useful, so survivors are leads, not proof.
• Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation: Type-checked Lean specs can still misstate intent, so the paper scores specs on validity, reference equivalence via BEq+, and behavioral adequacy such as accepting valid and rejecting invalid inputs.
• Natural Language based Specification and Verification: Typed natural-language contract records written and judged by an LLM make a high-recall bug finder but not a sound verifier, since nothing is proved.
• What is Formal Verification without Specifications? A Survey on mining LTL Specifications: Surveys passive learning of LTL from positive and negative traces, comparing constraint-based, enumeration-based, and neural search; no common experimental benchmark.
• Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning: NFV translates NL claims about Python into frozen Dafny artifacts and issues 128 of 206 proofs with 92.2% precision, but intent is not checked, only the frozen artifact.
• GDPR Auto-Formalization with AI Agents and Human Verification: Turns GDPR articles into linked scenarios, atomic facts, rule trees, and labels, with human checks for faithful normative representation.
• Using LLMs to Facilitate Formal Verification of RTL: GPT-4 writes SystemVerilog assertions from RTL alone, JasperGold checks them, and humans audit, but full coverage does not show the assertions are correct.
• miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward: A full miniF2F audit found over 300 Lean statements corrected; a proof of a weakened statement earns no credit, and end-to-end accuracy is 34.8% without faithful autoformalization.
• OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification: Freeze the declarative safety invariant and let the agent generate only the transition, which prevents passing by weakening the property; a refinement relation is still needed.
• AfterVibe: What Remains When the Conversation Ends: Recovers a behavioral spec from diff and conversation; spec quality is whether a blind agent regenerates passing code, and verification conditions come from the trajectory, never the spec.
• Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification: Enumerating LTL formulas, paraphrasing them into English, and fine-tuning BART with constrained decoding yields 75% NL-to-LTL accuracy with little labeled data.
• A New Approach Towards Autoformalization: Staged autoformalization for research-level mathematics: unlinked formalization, entity linking, then type adjustment.
• MathAtlas: A Benchmark for Autoformalization in the Wild: MathAtlas gives about 52k textbook entities and 178k dependency relations for Lean autoformalization; scoring requires both compilation and faithfulness, since compiling alone is insufficient.
• Path2Spec: Path-Aware Specification Generation via Large Language Models: Path-first spec generation verified 325 of 385 programs versus 197 for SpecGen, but “verified” means OpenJML exit 0, not spec completeness.
• DSpec2Test: Specification-Driven Test Generation in Dafny: DSpec2Test generates Dafny black-box tests from requires and ensures by splitting contracts into mutually exclusive feasible classes, avoiding crashes from unguarded implications.
• Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning: Verified proofs guarantee validity, not formalization faithfulness: an unfaithful axiom such as “Fly Tweety” can make a Lean proof compile.
• What Good Are Strong Specifications?: Model-based contracts as executable oracles reportedly find twice as many faults as standard contracts, though 46% of 164 invariant clauses are internal representation constraints.
• A fully verified container library: EiffelBase2 (8440 lines, 1.4 spec lines per code line) is fully verified with AutoProof; interfaces use a ghost model attribute, with command postconditions on model updates and queries as pure model functions.
• Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications: Natural Hoare Logic links a parsed natural-language requirement’s logical form to program variables, then reduces verification to Hoare triples; the semantic parser itself is not proved correct.
• Talk is Cheap, Logic is Hard: Benchmarking LLMs on Post-Condition Formalization: Models turn NL descriptions into executable pre and postconditions, and no model solved all tasks in 10 attempts; a full postcondition must accept every correct output and reject every wrong one.
• PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation: An LLM writes properties in a small intermediate language that is compiled against the contract, rejecting undefined variables and ill-formed properties, and retrieves examples by embedded critical code.
• NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models: An LLM builds a first-order-logic syntax tree that a deterministic compiler emits as SMT-LIB, avoiding direct SMT generation.
• Primrose: Selecting Container Data Types by Their Properties: Primrose selects Rust container types using refinement types that combine syntactic traits with semantic predicates such as uniqueness or LIFO order.
• Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving: Isabelle checks LLM-written explanation axioms, and syntax errors go back to the LLM for repair over a fixed number of rounds.
• Autoformalizing Argumentative Material Inferences: Adding LLM-chosen guard assumptions made premises entail claims in Isabelle, but guards are assumptions not shown true, so faithfulness rests on tests.
• NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic: NeuroNL2LTL translates requirements to LTL via a structure-preserving intermediate language, where Spot checks guarantee satisfiability and non-triviality but not that the formula means the intended requirement.
• Re:Form – Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny: RL for Dafny spec generation uses the verifier as the only reward; spec infilling was rejected because models struggled to place clauses, so the task outputs full annotated code.
• Towards Neuro-symbolic Causal Rule Synthesis, Verification, and Evaluation Grounded in Legal and Safety Principles: An LLM proposes candidate first-order causal rules, and a validator checks syntax, logical consistency, and safety before rules enter the knowledge base.
• Inference of Properties from Requirements and Automation of Their Formal Verification: Planned project: infer declarative property specs from engineer-given examples and verify them at model and code level; no evaluation.
• Assisted Specification of Code Using Search: ASCUS mines repositories to propose checkable specifications for a subsystem, from test cases and abstracted candidate code.
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories: Human repair was needed throughout the LLM pipeline mapping math papers to PVS, including changing a theorem from surjective to bijective mapping.
• Self-Spec Verifiable Code Generation: Verifier acceptance does not mean the spec captures the requirement: on Rust direct generation, joint success is 57 versus 91 for validity, because coverage is only 0.697 with self-written specs.
• STAFF: Towards Translating Formal Verification Benchmarks between Formal Specification Languages: Translating verified Dafny to ACSL-annotated C took 113 of 162 programs to verification on the first pass and 130 after a repair loop that shows only failing C code and Frama-C errors.
• Towards platform-independent verification of the standard mathematical functions: the square root function?: Replace the exact sqrt postcondition with a parameterized error bound Eps, removing platform-dependent ulp requirements from the spec.
• Refinement Type Contracts for Verification of Scientific Investigative Software: Paranoid Scientist checks refinement-type contracts at runtime and found four bugs in a 3000-line scientific package, at 1.05-6.41x slowdown.
• Confidently Wrong: Exception Chain Collapse in Frontier LLM Rule Evaluation: The Aethis module compiles rules to SMT for deterministic evaluation; frontier LLMs give confident false negatives on nested exception chains.
• Beyond Solver Verdicts: Generative Reward Models for Autoformalization: Verdict-preserving unfaithfulness shows a solver verdict cannot certify faithfulness, since flipping > to < keeps the verdict, so a bidirectional Z3 oracle needs a gold reference.
• Conjecturing: An Overlooked Step in Formal Mathematical Reasoning: Formal reasoning often needs the answer itself, and a proof can validate an incomplete answer, such as one omitting x = 4, so specification completeness needs checking before proving.
• Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version): One Gospel contract feeds test, auto-proof, and interactive proof, and Ortac runs random state-machine traces to catch wrong contracts before proof effort.
• PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs: Translates PDE control requests into STL, proposes subgoals, and synthesizes control programs; measured on 1-D heat and wave systems, not proven correct.
• Towards Richer Challenge Problems for Scientific Computing Correctness: Position: challenge problems for scientific computing should cover layered correctness requirements, assumptions, validation, and scale.
• Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specifications: A verifier accepting a spec shows only that code matches the contract, so specs need separate test and mutation scores, since a weak requires clause can still pass OpenJML.
• SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications: SpecAgent’s agentic ACSL synthesis discharges 604 of 811 verification targets (74.5%) at 96.82% precision, with dependency-aware planning before writing contracts as one of four components.
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models: SpecGen runs a conversational generate-verify-repair loop with OpenJML feedback and then exhaustively mutates near-miss specs; 279 of 385 programs get verifiable specs, measured by verifier acceptance and expert rating.
• SpecPylot: Python Specification Generation using Large Language Models: LLM-added Python contracts only survive bounded CrossHair search; PASSED is not a proof, and the paper measures survival on 20 programs.
• SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis: Test-based completeness rewards for Dafny specs raised completeness from 18.15 to 24.30 at pass@1 for a 7B model, using mutated outputs that the implementation cannot produce.
• SpecSyn: specification recovery through decomposition and mutation: SpecSyn generates ACSL contracts for C given target assertions, and decomposition by dependency SCCs is the largest gain, lifting gpt-5 recall from 63.25% to 75.91%.
• TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation: A TLA+ spec generator rewarded directly by TLC gained from a mutation check that breaks each invariant, which catches tautologies like TypeOK == TRUE, while weak non-tautological invariants survive.
• Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation: An LLM drafted ACSL contracts that a PETSc expert certified, and verification found a MatAYPX aliasing bug present since 1997, with a deterministic compiler writing the driver.
• Gradual Verification for Smart Contracts: Gradual verification for pyTEAL contracts combines optimistic static checks with generated runtime checks, so specs can be added incrementally.
• ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees: Iterative LLM question-answering translates natural-language robot tasks into LTL with a conformal guarantee of equivalence probability at least 1 minus alpha.
• Agentic Separation Logic Specification Synthesis: A spec-agent synthesizes pre and postconditions for C++ repos, with fuzzing rejecting wrong specs by counterexample but proving nothing, and the best model reaches 85.87% test-valid on BDE.
• Verifiable Checks for Business Rule Consistency: SIRNA translates business docs to SMT-LIB, a deterministic encoder handles the DSL, and Z3 checks equivalence, with voting separating autoformalization failures from semantic mismatches.
• Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications: LLM extraction of atomic requirements from informal specs matched or partially matched 81.8% of 55 generated requirements, and syntax checks alone do not show intent match.
• Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python: Why3-py translates annotated Python to WhyML under Belief Hoare Logic, verifying correct use of statistical methods rather than library implementations.
• Teaching Code LLMs to Reason with Intermediate Formal Specifications: Executable checkpoint assertions at internal program points help only if they hold on correct runs and reject faulty ones, catching wrong intermediate algorithms that a final postcondition misses.
• Improving Symbolic Translation of Language Models for Logical Reasoning: Filtering LLM-generated FOL translations by Prover9 parsing and label match left about 2% manually found errors in a 50-record check, though the filter only confirms solver outputs.
• Aligning Requirement for Large Language Model’s Code Generation: Spec misalignment is detected when public tests fail, and generated tests count only as tie-breakers, since they are only 60 to 73% accurate.
• Unfolding Iterators: Specification and Verification of Higher-Order Iterators in OCaml: A passing client proof assumes the iterator contract, so iterator contracts are trusted unless the iterator implementation is verified too.
• Supporting Software Formal Verification with Large Language Models: An Experimental Study: SpecVerify has two LLM stages from requirement to C assertions checked by ESBMC; 46 of 58 generated properties matched manual ones (79.31%), and the pipeline ran without human review.
• AUTO CEDAR: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis: AUTO CEDAR fixes floors, ceilings, and liveness slices before any LLM policy search, and the model cannot edit them, so a synthesis theorem bounds accepted policies.
• Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon: Kernel contracts state precision, shape, ordering, tolerance, and exceptional values, so disagreeing kernels are judged by the contracts they claim.
• Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs: Predicate extraction is the main NL-to-FOL bottleneck, since a gold predicate list raises exact match from 35.8% to 63.5% while a tokenizer extension gains under 1 point.
• Auditing Framework APIs via Inferred App-side Security Specifications: Bluebird infers API sensitivity from app-side checks, combining NLP with static analysis of the calling apps.
• First Experiments with Neural Translation of Informal to Formal Mathematics: Early seq2seq autoformalization reaches 65.73% exact match on Mizar pairs, but it measures string match, not proof checking, and its synthetic pairs come from a formal corpus.
• KerSpecGen: Co-piloting formal Kernel specification synthesis with refined knowledge graphs and large language models: KerSpecGen generates Isabelle/HOL seL4 specs from requirements through a knowledge graph, but its output is never executed or verified, only scored by similarity and experts.
• Preguss: It Analyzes, It Specifies, It Verifies: This position paper splits runtime-error verification into analysis, LLM spec synthesis, and deductive proof of units, but no implementation was evaluated.
• FormalRx: Rectify and eXamine Semantic Failures in Autoformalization: FormalRx diagnoses autoformalization with an aligned flag, an error category, a location, and a corrected statement, from a 28-category taxonomy.
• Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning: LLM legal reasoning is often unfaithful to the solver: scope laundering reports entailment where the solver gives neutral, in 15.3% to 52.5% of cases, so check results against the formal input.
• When Specifications Conflict: A Symmetry-Based Framework for Measuring LLM Preferences: When a formal spec conflicts with an NL spec, LLMs follow the formal one at 87.45% and io examples are followed less, so formal artifacts dominate in prompts.
• Automatic Generation of Specifications using Verification Tools: Thesis: auto-generates loop invariants and method contracts for KeY via abstract interpretation with symbolic execution; widening forces termination, and the fixed point is sound by construction.
• Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory: Compiling does not show a theorem matches its source: an audit with verbatim quotes classifies each hypothesis as in-source, implied, or potential drift.
• Model-Driven Discipline for Multi-Agent LLMs: Requirement-to-Verification Generation of Traceable System Models: LLM agents gained syntactic validity from requirement models to checked behavior models, but execution gains were inconsistent across models, so syntax is the only robust win.
• Towards Deriving Verification Properties: English tenets, a goal tree, and domain implications yield LTL properties for model checking; richer logics are harder to verify.
• StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs Through Knowledge-Reasoning Fusion: Autoformalization training data was selected by Lean syntax checks and equivalence voting over 16 candidates, giving about 183K pairs with no reported human correctness check.
• VIVERRA: Text-to-Code with Guarantees: VIVERRA has an LLM write C with assertions checked by bounded model checkers; the guarantee holds only up to loop bound k=5 and does not prove the program matches the task.
• Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction: Turning API documentation into formal specs through staged agents with deterministic checks, where removing any single stage dropped precision to 0.06 to 0.26, so every stage is necessary.
• NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry: Auto-formalization is judged by execution: AlphaGeometry must run and yield a valid spec, and 54 few-shot examples lift every model that scored above 0.
• FMC: Formalization of Natural Language Mathematical Competition Problems: FMC is a training-free NL-to-Lean statement pipeline reaching 93.39% compile and 81.74% consistency after error-feedback retries, at a cost of 161M tokens.
• Towards Automated Formal Verification of Backend Systems with LLMs: Scala backend to Lean needs the DB state as an explicit parameter, and a proof shows logic is correct only if translation and theorem statements preserve intent.
• Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization: A reference-free proxy judge checks a vector of per-axis properties and repairs the failed axis, with geometric convergence under bounded judge noise.
• LLM-Assisted Formalization Enables Deterministic Detection of Statutory Inconsistency in the Internal Revenue Code: LLM formalizes a tax statute into Prolog while a deterministic engine detects inconsistency, separating probabilistic formalization from checking.
• Verification-Guided Specification Synthesis with Large Language Models for Intrusion Detection Rules: An LLM proposes a Python predicate for each attack, and a deterministic compiler emits the IDS rule.
• Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization: Lean formalizations can type-check yet mean something else, such as an omitted annotation making 3 / 2 = 1.5 infer Nat, so the paper tracks human-verified declarations in a manifest.
• Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications: SESpec combines symbolic execution, invariant templates, an LLM, and Frama-C to verify 354 of 395 C/ACSL programs, but solves 0 of 3 programs with external or recursive calls.
• How Powerful Are LLMs in Generating Formal Program Specifications?: COINS grades spec quality separately from proof difficulty: a candidate spec fails if a mutant is provably accepted, since positive proofs alone accept overly permissive specs.
• Generating Precise Format Specification for Network Protocols Through Adversarial LLM Interactions: Adversarial interaction between a format spec and a reference parser refines both to a fixed point, which is evidence of agreement, not proof.
• Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version): Pika functional specs translate to SuSLik, enabling push-button synthesis of C programs with in-place updates and full separation-logic proofs.
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models: Compile-only statements survive at 92.4%, but a semantic check cuts them to 31.7%, so meaning filtering, not compilation, is the bottleneck.
• Generating Symbolic World Models via Test-time Scaling of Large Language Models: LLMs generate PDDL domains with extra inference compute; VAL checks syntax and plan executability, not that the domain matches intent.
• Mathesis: Towards Formal Theorem Proving from Natural Languages: Mathesis checks semantics separately from the proof, catching drift such as a desired conclusion added as an assumption, and its proof gate rejects vacuous statements.
• VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code: Scores generated Dafny code and specs in both directions, checking that the code satisfies the spec and that the spec’s behaviors are realized, over 2,389 problems.
• An Agile Formal Specification Language Design Based on K Framework: ASL is a YAML and K-syntax spec language compiled to K; fewer spec lines than K do not show that the spec expresses intent.
• Automated Extraction of Protocol State Machines from 3GPP Specifications with Domain-Informed Prompts and LLM Ensembles: SpecGPT extracts protocol state machines from 3GPP specs with LLM ensembles; agreement with a reference does not prove true behavior.
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems: Decomposing a statement into concept queries with guessed Lean names, then retrieving premises, raised GPT-4.1’s ConNF BEq+@10 from 6.76% zero-shot to 62.33%.
• Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning: Ensemble of LLM judges scores logical preservation, consistency, and formal quality of autoformalizations; theorem provers check validity, with no reference formalization.
• KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment: KELPS maps NL math to a Knowledge Equation IR of a=b assertions, then converts to Lean, Coq, or Isabelle using expert rules.
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization: Compiling is not faithful: a full agent compiles 87.2% of 227 graduate statements but only 57.7% are faithful, a 29.5-point gap, judged by LLM graders calibrated against humans.
• Monotonic Reference-Free Refinement for Autoformalization: A monotonic objective makes an invalid candidate score zero, since prover validity multiplies the judge scores, but judges do not prove the statement preserves the NL theorem.
• Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications: Generating separation-logic memory specs with predicate docs, few-shot examples, and compiler-feedback repair for two error classes, though the paper gives no quantitative results.
• Theory-Scale Auto-Formalization of Logics for Computer Science: Best item-level autoformalization of a logic textbook passed only 20.1% of items, which motivates planning embedding levels with a concept graph before coding.

Last edited: 2026-11-06