{"total":57,"rows":[{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49,"area":null},{"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":"2505.13938","title":"CLEVER: A Curated Benchmark for Formally Verified Code Generation","created":"2025-05-20","cited_by_count":29,"area":null},{"id":"2508.11126","title":"AI Agentic Programming: A Survey of Techniques, Challenges, and Opportunities","created":"2025-08-15","cited_by_count":28,"area":"agents"},{"id":"2504.05408","title":"Frontier AI's Impact on the Cybersecurity Landscape","created":"2025-04-07","cited_by_count":21,"area":null},{"id":"2509.22908","title":"A benchmark for vericoding: formally verified program synthesis","created":"2025-09-26","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":"2502.05252","title":"GSM-Infinite: How Do Your LLMs Behave over Infinitely Increasing Context Length and Reasoning Complexity?","created":"2025-02-07","cited_by_count":17,"area":"lr"},{"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":"2602.09464","title":"AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms","created":"2026-02-10","cited_by_count":12,"area":null},{"id":"2411.15143","title":"dafny-annotator: AI-Assisted Verification of Dafny Programs","created":"2024-11-05","cited_by_count":8,"area":null},{"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":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","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":"2510.06296","title":"VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code","created":"2025-10-07","cited_by_count":7,"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":"2509.23061","title":"Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification","created":"2025-09-27","cited_by_count":6,"area":null},{"id":"2511.17330","title":"Agentic Verification of Software Systems","created":"2025-11-21","cited_by_count":6,"area":"agents"},{"id":"2509.25197","title":"Towards Repository-Level Program Verification with Large Language Models","created":"2025-08-31","cited_by_count":4,"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":"2604.12268","title":"CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation","created":"2026-04-14","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":"2508.18587","title":"A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants","created":"2025-08-26","cited_by_count":3,"area":null},{"id":"2602.01075","title":"ConvexBench: Can LLMs Recognize Convex Functions?","created":"2026-02-01","cited_by_count":3,"area":null},{"id":"2605.08553","title":"VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation","created":"2026-05-08","cited_by_count":3,"area":null},{"id":"2502.11901","title":"Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity","created":"2025-02-17","cited_by_count":2,"area":"lr"},{"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.16584","title":"Certified Program Synthesis with a Multi-Modal Verifier","created":"2026-04-17","cited_by_count":2,"area":null},{"id":"2608.09277","title":"P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation","created":"2026-08-10","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":"2506.10998","title":"Towards Automated Formal Verification of Backend Systems with LLMs","created":"2025-04-13","cited_by_count":1,"area":null},{"id":"2509.06239","title":"Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning","created":"2025-09-07","cited_by_count":1,"area":"lr"},{"id":"2512.02080","title":"The 4/$\\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee","created":"2025-11-30","cited_by_count":1,"area":null},{"id":"2601.02060","title":"Perish or Flourish? A Holistic Evaluation of Large Language Models for Code Generation in Functional Programming","created":"2026-01-05","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":"2606.32007","title":"AxDafny: Agentic Verified Code Generation in Dafny","created":"2026-06-30","cited_by_count":1,"area":"agents"},{"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":"2602.20979","title":"Toward an Agentic Infused Software Ecosystem","created":"2026-02-24","cited_by_count":0,"area":"agents"},{"id":"2604.22601","title":"From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification","created":"2026-04-24","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.27485","title":"Automating Formal Verification with Agent-Guided Tree Search","created":"2026-05-26","cited_by_count":0,"area":"agents"},{"id":"2606.01008","title":"FVSpec: Real-World Property-Based Tests as Lean Challenges","created":"2026-05-31","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.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":"2607.27733","title":"VeriSkill: A Self-Evolution Framework for Program Verification Skills","created":"2026-07-30","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.19391","title":"MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs","created":"2026-09-16","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.31874","title":"COUNTERMEM: World-Model Verified Counter-Factual Memory for Language Agents","created":"2026-09-25","cited_by_count":0,"area":"wm"},{"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.14923","title":"TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents","created":"2026-10-10","cited_by_count":0,"area":"agents"},{"id":"2610.15258","title":"Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning","created":"2026-10-11","cited_by_count":0,"area":"agents"}],"next_cursor":null}