{"total":67,"rows":[{"id":"2502.01718","title":"ACECODER: Acing Coder RL via Automated Test-Case Synthesis","created":"2025-02-03","cited_by_count":93,"area":"lr"},{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2409.09030","title":"Agents in Software Engineering: Survey, Landscape, and Vision","created":"2024-09-13","cited_by_count":60,"area":"agents"},{"id":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2406.08467","title":"DafnyBench: A Benchmark for Formal Software Verification","created":"2024-06-12","cited_by_count":57,"area":null},{"id":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49,"area":null},{"id":"2412.06176","title":"AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement","created":"2024-12-09","cited_by_count":35,"area":"synth"},{"id":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","cited_by_count":34,"area":null},{"id":"2410.15756","title":"Automated Proof Generation for Rust Code via Self-Evolution","created":"2024-10-21","cited_by_count":33,"area":null},{"id":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","cited_by_count":20,"area":null},{"id":"2502.05714","title":"Proving the Coding Interview: A Benchmark for Formally Verified Code Generation","created":"2025-02-08","cited_by_count":19,"area":null},{"id":"2501.16207","title":"From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs","created":"2025-01-27","cited_by_count":18,"area":"lr"},{"id":"2512.17661","title":"Vidarc: Embodied Video Diffusion Model for Closed-loop Control","created":"2025-12-19","cited_by_count":15,"area":"diffusion"},{"id":"2512.18436","title":"VeruSAGE: A Study of Agent-Based Verification for Rust Systems","created":"2025-12-20","cited_by_count":12,"area":"agents"},{"id":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","cited_by_count":11,"area":null},{"id":"2403.03997","title":"Guiding Enumerative Program Synthesis with Large Language Models","created":"2024-03-06","cited_by_count":9,"area":null},{"id":"2510.25015","title":"VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus","created":"2025-10-28","cited_by_count":9,"area":null},{"id":"2511.12294","title":"ProofWright: Towards Agentic Formal Verification of CUDA","created":"2025-11-15","cited_by_count":9,"area":"agents"},{"id":"2603.17150","title":"Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents","created":"2026-03-17","cited_by_count":9,"area":"agents"},{"id":"2504.20964","title":"OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification","created":"2025-04-29","cited_by_count":8,"area":null},{"id":"2603.25111","title":"SEVerA: Verified Synthesis of Self-Evolving Agents","created":"2026-03-26","cited_by_count":8,"area":"agents"},{"id":"2604.25031","title":"Faithful Autoformalization via Roundtrip Verification and Repair","created":"2026-04-27","cited_by_count":8,"area":null},{"id":"2410.14865","title":"Joint Verification and Refinement of Language Models for Safety-Constrained Planning","created":"2024-10-18","cited_by_count":6,"area":null},{"id":"2501.06283","title":"Dafny as Verification-Aware Intermediate Language for Code Generation","created":"2025-01-10","cited_by_count":6,"area":null},{"id":"2511.00125","title":"Inferring multiple helper Dafny assertions with LLMs","created":"2025-10-31","cited_by_count":4,"area":null},{"id":"2601.18944","title":"Neural Theorem Proving for Verification Conditions: A Real-World Benchmark","created":"2026-01-26","cited_by_count":4,"area":null},{"id":"2605.23109","title":"Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems","created":"2026-05-22","cited_by_count":4,"area":null},{"id":"2403.18327","title":"$\\forall$uto$\\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks","created":"2024-03-27","cited_by_count":3,"area":null},{"id":"2502.01573","title":"Next Steps in LLM-Supported Java Verification","created":"2025-02-03","cited_by_count":3,"area":null},{"id":"2503.14183","title":"Can LLMs Enable Verification in Mainstream Programming?","created":"2025-03-18","cited_by_count":3,"area":null},{"id":"2603.00805","title":"NERFIFY: A Multi-Agent Framework for Turning NeRF Papers into Code","created":"2026-02-28","cited_by_count":3,"area":"agents"},{"id":"2605.26457","title":"Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization","created":"2026-05-26","cited_by_count":3,"area":"agents"},{"id":"2404.09384","title":"Generative transformations and patterns in LLM-native approaches for software verification and falsification","created":"2024-04-14","cited_by_count":2,"area":null},{"id":"2507.15822","title":"Do AI models help produce verified bug fixes?","created":"2025-07-21","cited_by_count":2,"area":null},{"id":"2512.10187","title":"MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification","created":"2025-12-11","cited_by_count":2,"area":"lr"},{"id":"2602.04892","title":"Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction","created":"2026-01-30","cited_by_count":2,"area":null},{"id":"2604.00280","title":"Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability","created":"2026-03-31","cited_by_count":2,"area":null},{"id":"2604.10392","title":"Intent-aligned Formal Specification Synthesis via Traceable Refinement","created":"2026-04-12","cited_by_count":2,"area":null},{"id":"2604.16584","title":"Certified Program Synthesis with a Multi-Modal Verifier","created":"2026-04-17","cited_by_count":2,"area":null},{"id":"2608.13522","title":"Vero: Can AI Agents Build Formally Verified Software Repositories?","created":"2026-08-13","cited_by_count":2,"area":null},{"id":"2410.18494","title":"Assured Automatic Programming via Large Language Models","created":"2024-10-24","cited_by_count":1,"area":null},{"id":"2501.06370","title":"Towards a Probabilistic Framework for Analyzing and Improving LLM-Enabled Software","created":"2025-01-10","cited_by_count":1,"area":null},{"id":"2605.17246","title":"Fidelity Probes for Specification--Code Alignment","created":"2026-05-17","cited_by_count":1,"area":null},{"id":"2605.30914","title":"Automating Formal Verification with Reinforcement Learning and Recursive Inference","created":"2026-05-29","cited_by_count":1,"area":"lr"},{"id":"2607.04631","title":"Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs","created":"2026-07-06","cited_by_count":1,"area":null},{"id":"2501.05252","title":"From Scientific Texts to Verifiable Code: Automating the Process with Transformers","created":"2025-01-09","cited_by_count":0,"area":null},{"id":"2501.12972","title":"Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs","created":"2025-01-22","cited_by_count":0,"area":null},{"id":"2507.12443","title":"LLM-Based Config Synthesis requires Disambiguation","created":"2025-07-16","cited_by_count":0,"area":null},{"id":"2509.09194","title":"On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability","created":"2025-09-11","cited_by_count":0,"area":null},{"id":"2605.07935","title":"TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples","created":"2026-05-08","cited_by_count":0,"area":"agents"},{"id":"2605.14972","title":"Viverra: Text-to-Code with Guarantees","created":"2026-05-14","cited_by_count":0,"area":null},{"id":"2605.22368","title":"VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation","created":"2026-05-21","cited_by_count":0,"area":null},{"id":"2605.30054","title":"Projectional Decoding: Towards Semantic-Aware LLM Generation","created":"2026-05-28","cited_by_count":0,"area":null},{"id":"2607.01585","title":"ADVENT: LLM-Driven Automatic Predicate Invention for ILP","created":"2026-07-02","cited_by_count":0,"area":null},{"id":"2607.09366","title":"Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability","created":"2026-07-10","cited_by_count":0,"area":null},{"id":"2607.14137","title":"Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations","created":"2026-07-10","cited_by_count":0,"area":null},{"id":"2607.23425","title":"TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation","created":"2026-07-26","cited_by_count":0,"area":null},{"id":"2608.00965","title":"An AI Approach to Verified Production Cryptographic Libraries","created":"2026-08-02","cited_by_count":0,"area":null},{"id":"2608.03588","title":"GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation","created":"2026-08-04","cited_by_count":0,"area":"agents"},{"id":"2608.29841","title":"SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs","created":"2026-08-30","cited_by_count":0,"area":"agents"},{"id":"2609.23954","title":"Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler","created":"2026-09-21","cited_by_count":0,"area":null},{"id":"2609.25018","title":"OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agents","created":"2026-08-08","cited_by_count":0,"area":"agents"},{"id":"2609.31687","title":"Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation","created":"2026-09-16","cited_by_count":0,"area":null},{"id":"2609.39022","title":"From Verification Failures to Reusable Guidance for Coding Agents","created":"2026-09-30","cited_by_count":0,"area":"agents"},{"id":"2610.09159","title":"SpecGuard: Proving a Task Is Broken Before the Agent Cheats","created":"2026-10-06","cited_by_count":0,"area":"agents"},{"id":"2610.15797","title":"Passing Tests, Missing Semantics: Evidence of Interpretive Lock-In in Plan-Based DataFrame Code Generation","created":"2026-10-11","cited_by_count":0,"area":null},{"id":"2610.17358","title":"claimcheck: Measuring and Improving Specification Faithfulness","created":"2026-10-12","cited_by_count":0,"area":null}],"next_cursor":null}