Formal Verification

Ask about this topic

Overview

Formal verification studies rigorous ways to show that systems satisfy properties such as safety, security, and correctness. It represents systems and requirements with logic, then uses theorem proving, model checking, SMT solving, static analysis, and runtime monitoring to prove properties or find counterexamples. These methods apply to software, hardware, protocols, neural networks, robotics, and AI agents, where failures can be costly and testing covers only selected executions. Current work combines automation and language models to reduce proof effort, but scalability and whether specifications faithfully capture intended behavior remain central challenges.

Latest papers

CardsList

354 papers46 papers in the last four weeks, up 21% on the four weeks before. 0.3% of all new papers.

  1. Pipeline for Verifying LLM-Generated Mathematical Solutions

    Feb 24, 2026Varvara Sazonova, Dmitri Shmelkin, Stanislav Kikot +1LLM Answer VerificationLLM Evaluation

    Moscow State University · Huawei Technologies Co., Ltd

  2. The LLMbda Calculus: AI Agents, Conversations, and Information Flow

    Feb 23, 2026Zac Garby, Andrew D. Gordon, David SandsPrompt Injection Attacks on AI AgentsLLM Agent Harnesses

    University of Nottingham, Nottingham, UK · University of Edinburgh, Edinburgh, UK · Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden

  3. Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic

    Feb 20, 2026Michal Töpfer, František Plášil, Tomáš Bureš +1Temporal LogicLLM-Based Program Synthesis

    Charles University, Czech Republic

  4. 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

  5. BMC4TimeSec: Verification Of Timed Security Protocols

    Feb 19, 2026Agnieszka M. ZbrzeznyBounded Model CheckingFormal Verification

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

  6. 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

  7. 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

  8. 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

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

    Feb 16, 2026Dennis GrossFormal Methods for RLFormal Verification

  10. Formal Evidence Generation for Assurance Cases for Robotic Software Models

    Feb 3, 2026Fang Yan, Simon Foster, Ana Cavalcanti +2AI AssuranceRobot Safety

    University of York, York, UK

  11. 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

  12. 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

  13. Verification of Unknown Dynamical Systems via Autoencoder Latent Space

    Dec 15, 2025Robert Reed, Luca Laurenti, Morteza LahijanianFormal VerificationState Abstraction

    Dept. of Aerospace Engineering University of Colorado Boulder Boulder, Colorado, USA · Delft University of Technology Delft, Netherlands · AI4I, Turin, Italy

  14. 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

  15. 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.

  16. Synthesis and Verification of Register Automata over Data Sequences (Technical Report)

    Nov 24, 2025Chih-Duo Hong, Hongjian Jiang, Anthony W. Lin +3Formal VerificationInterpretable ML

    National Chengchi University, Taipei, Taiwan · University of Kaiserslautern-Landau, Kaiserslautern, Germany · MPI-SWS, Kaiserslautern, Germany +1

  17. 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

  18. 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

  19. 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

  20. ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems

    Nov 4, 2025Eric Vin, Lucy Horowitz, Kyle A. Miller +3Formal VerificationAI Assurance

    University of California, Santa Cruz, Santa Cruz CA 95064, USA · University of Michigan, Ann Arbor MI 48109, USA · University of California, Berkeley, Berkeley CA 94720, USA

  21. 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

  22. 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

  23. 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

  24. 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