{"total":58,"rows":[{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"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":"2508.16546","title":"RL Is Neither a Panacea Nor a Mirage: Understanding Supervised vs. Reinforcement Learning Fine-Tuning for LLMs","created":"2025-08-22","cited_by_count":17,"area":null},{"id":"2512.18160","title":"Propose, Solve, Verify: Self-Play Through Formal Verification","created":"2025-12-20","cited_by_count":13,"area":"synth"},{"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":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","cited_by_count":11,"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":"2406.10903","title":"New Solutions on LLM Acceleration, Optimization, and Application","created":"2024-06-16","cited_by_count":7,"area":null},{"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":"2406.03636","title":"Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages","created":"2024-06-05","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":"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":"2502.05344","title":"RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation","created":"2025-02-07","cited_by_count":4,"area":"rag"},{"id":"2504.11711","title":"The Hitchhiker's Guide to Program Analysis, Part II: Deep Thoughts by LLMs","created":"2025-04-16","cited_by_count":4,"area":null},{"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":"2503.14183","title":"Can LLMs Enable Verification in Mainstream Programming?","created":"2025-03-18","cited_by_count":3,"area":null},{"id":"2604.03758","title":"AutoReSpec: A Framework for Generating Specification using Large Language Models","created":"2026-04-04","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":"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":"2502.15217","title":"FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs","created":"2025-02-21","cited_by_count":2,"area":null},{"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":"2410.18494","title":"Assured Automatic Programming via Large Language Models","created":"2024-10-24","cited_by_count":1,"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":"2511.06552","title":"LLM For Loop Invariant Generation and Fixing: How Far Are We?","created":"2025-11-09","cited_by_count":1,"area":null},{"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":"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":"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":"2506.14627","title":"Working Document -- Formalising Software Requirements with Large Language Models","created":"2025-06-17","cited_by_count":0,"area":null},{"id":"2512.07501","title":"AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution","created":"2025-12-08","cited_by_count":0,"area":null},{"id":"2602.20979","title":"Toward an Agentic Infused Software Ecosystem","created":"2026-02-24","cited_by_count":0,"area":"agents"},{"id":"2603.18334","title":"Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought","created":"2026-03-18","cited_by_count":0,"area":"lr"},{"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.01394","title":"LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation","created":"2026-05-02","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":"2606.26490","title":"An Empirical Study of LLM-Generated Specifications for VeriFast","created":"2026-06-25","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":"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.34886","title":"Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.39568","title":"Self-Spec Verifiable Code Generation","created":"2026-09-30","cited_by_count":0,"area":null}],"next_cursor":null}