Formal Verification

Ask about this topic

Latest papers 317

44 papers in the last four weeks, up 91% on the four weeks before. 0.3% of all new papers.

All topics
CardsList

  1. VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean

    Feb 20, 2026Yutong Xin, Qiaochu Chen, Greg Durrett +1LLM EvaluationFormal Verification

    The University of Texas at Austin · New York University

  2. BMC4TimeSec: Verification Of Timed Security Protocols

    Feb 19, 2026Agnieszka M. ZbrzeznyFormal Verification

    Department of Computer Science, Faculty of Design, SWPS University, Warsaw, Poland

  3. M2F: Automated Formalization of Mathematical Literature at Scale

    Feb 19, 2026Zichen Wang, Wanli Ma, Zhenyu Ming +3AutoformalizationFormal Verification

    School of Mathematical Sciences, Peking University · Beijing International Center for Mathematical Research, Peking University · Huawei Technologies +1

  4. MerLean: An Agentic Framework for Autoformalization in Quantum Computation

    Feb 18, 2026Yuanjie Ren, Jinzheng Li, Yidi QiAutoformalizationFormal Verification

    Massachusetts Institute of Technology Cambridge, MA 02139 · Northeastern University Boston, MA 02115

  5. Synthesis and Verification of Transformer Programs (Technical Report)

    Feb 18, 2026Hongjian Jiang, Matthew Hague, Philipp Rümmer +1Program SynthesisFormal Verification

    University of Kaiserslautern-Landau, Germany · Royal Holloway, University of London, England · Uppsala University, Sweden +2

  6. Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC

    Feb 16, 2026Dennis GrossFormal VerificationHealthcare

  7. Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction

    Jan 30, 2026Shihao Xia, Mengting He, Haomin Jia +2AutoformalizationProgram Synthesis

    The Pennsylvania State University · University of the Chinese Academy of Sciences · Institute of Computing Technology, Chinese Academy of Sciences

  8. LLMs versus the Halting Problem: Characterizing Program Termination Reasoning

    Jan 26, 2026Oren Sultan, Jordi Armengol-Estape, Pascal Kesseli +4LLM EvaluationStatic Code Analysis

    1Meta FAIR · 3Bloomberg, New York, USA · 4Imperial College London, UK +2

  9. MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

    Dec 11, 2025Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +1Automated Theorem ProvingFormal Verification

    University of Cambridge, Cambridge, UK · Amazon Web Services, London, UK · Amazon Web Services, Boston, USA

  10. The 4/δδ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

    Nov 30, 2025Pierre Dantas, Lucas Cordeiro, Youcheng Sun +1LLM Answer VerificationFormal Verification

    Dept. of Computer Science, The University of Manchester, UK. · Dept. of Electrical Engineering, Federal University of Amazonas (UFAM), Brazil.

  11. Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

    Nov 19, 2025Hiep Hong Trinh, Marjan Sirjani, Federico Ciccozzi +2Multi-Robot SystemsRobotics

    Mälardalen University, Universitetsplan 1, 721 23 Västerås, Sweden · KTH Royal Institute of Technology, Brinellvägen 8, 114 28 Stockholm, Sweden

  12. A Neurosymbolic Approach to Natural Language Formalization and Verification

    Nov 12, 2025Chenyang An, Sam Bayless, Stefano Buliani +27Formal VerificationLLM Safety

    Amazon Web Services · University College London · Queen Mary University of London +1

  13. Structural Enforcement of Statistical Rigor in AI-Driven Discovery: A Functional Architecture

    Nov 10, 2025Karen SargsyanFDR ControlFormal Verification

    aInstitute of Chemistry, Academia Sinica, Taipei, Taiwan

  14. Real-Time Model Checking for Closed-Loop Robot Reactive Planning

    Aug 26, 2025Christopher Chandler, Bernd Porr, Giulia Lafratta +1Safe Robot NavigationFormal Verification

    Department of Electronic and Electrical Engineering, University of Strathclyde, Glasgow, Scotland, UK · School of Engineering, University of Glasgow, Glasgow, Scotland, UK · School of Computing Science, University of Glasgow, Glasgow, Scotland, UK

  15. Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

    Jul 22, 2025Chuanhao Yan, Fengdi Che, Xuhan Huang +12RL for Language ModelsRL for Language Model Reasoning

    Shanghai AI Lab · Tsinghua University · University of Alberta +5

  16. HoarePrompt: Structural Reasoning About Program Correctness in Natural Language

    Mar 25, 2025Dimitrios Stamatios Bouras, Yihan Dai, Tairan Wang +2LLM PromptingFormal Verification

    Key Laboratory of HCST (PKU), MoE, SCS, Peking University Beijing, China · University College London London, United Kingdom

  17. Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

    Feb 5, 2024Till Hofmann, Stefan Schupp, Gerhard LakemeyerLogical ReasoningReachability Analysis

    RWTH Aachen University, Germany · University of Oxford, United Kingdom · TU Wien, Austria