{"total":38,"rows":[{"id":"2310.17807","title":"Clover: Closed-Loop Verifiable Code Generation","created":"2023-10-26","cited_by_count":67,"area":null},{"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":"2503.09002","title":"KNighter: Transforming Static Analysis with LLM-Synthesized Checkers","created":"2025-03-12","cited_by_count":24,"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":"2406.11915","title":"miniCodeProps: a Minimal Benchmark for Proving Code Properties","created":"2024-06-16","cited_by_count":18,"area":null},{"id":"2406.09757","title":"Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages","created":"2024-06-14","cited_by_count":16,"area":null},{"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":"2311.03739","title":"Leveraging Large Language Models for Automated Proof Synthesis in Rust","created":"2023-11-07","cited_by_count":11,"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":"2502.18917","title":"ClassInvGen: Class Invariant Synthesis using Large Language Models","created":"2025-02-26","cited_by_count":11,"area":null},{"id":"2603.19329","title":"Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification","created":"2026-03-18","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":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","cited_by_count":8,"area":null},{"id":"2411.02318","title":"Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast","created":"2024-11-04","cited_by_count":5,"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":"2601.18944","title":"Neural Theorem Proving for Verification Conditions: A Real-World Benchmark","created":"2026-01-26","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":"2608.03836","title":"Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers","created":"2026-08-04","cited_by_count":3,"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":"2603.03668","title":"Can LLM Aid in Solving Constraints with Inductive Definitions?","created":"2026-03-04","cited_by_count":1,"area":null},{"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":"2511.21104","title":"BRIDGE: Building Representations In Domain Guided Program Synthesis","created":"2025-11-26","cited_by_count":0,"area":null},{"id":"2604.27644","title":"ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoning","created":"2026-04-30","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.00965","title":"An AI Approach to Verified Production Cryptographic Libraries","created":"2026-08-02","cited_by_count":0,"area":null},{"id":"2608.13681","title":"Fine-Tuning Qwen3-27B for C-to-Rust Code Translation: A Three-Stage Curriculum of Pretraining, Debugging-Aware SFT, and Task-Specific SFT","created":"2026-08-13","cited_by_count":0,"area":null},{"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},{"id":"2610.03994","title":"Solving VeriContest with a Lean-Backed Rust Verifier","created":"2026-10-02","cited_by_count":0,"area":null}],"next_cursor":null}