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 320

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

All topics
CardsList

  1. Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

    Mar 26, 2026Partha Roop, Sobhan Chatterjee, Avinash Malik +2Signal Temporal LogicFormal Verification

    University of Auckland, Auckland, New Zealand · Auckland University of Technology, Auckland, New Zealand

  2. Decidable By Construction: Design-Time Verification for Truly Fearless Systems

    Mar 26, 2026Houston HaynesFormal Verification

    SpeakEZ Technologies, Asheville, NC

  3. Distribution and Clusters Approximations as Abstract Domains in Probabilistic Abstract Interpretation to Neural Network Analysis

    Mar 26, 2026Zhuofan Zhang, Herbert WiklickyNeural Network VerificationFormal Verification

    Department of Computing, Imperial College London, London, UK

  4. Probabilistic Abstract Interpretation on Neural Networks via Grids Approximation

    Mar 26, 2026Zhuofan Zhang, Herbert WiklickyNeural Network VerificationFormal Verification

    Imperial College London, 180 Queen’s Gate, South Kensington, London SW7 2AZ

  5. Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

    Mar 25, 2026Andreas SchlapbachAgent Communication ProtocolsFormal Verification

    Swiss Federal Railways (SBB) SBB IT Berne, Switzerland

  6. The SCAN Statistical Model Checker

    Mar 24, 2026Enrico Ghiorzi, Armando TacchellaFormal Verification

    Università di Genova

  7. Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains

    Mar 22, 2026Octavian UntilaFormal VerificationAI Agent Safety

    Aisophical SRL, Bucharest, Romania

  8. Neuro-Symbolic Proof Generation for Scaling Systems Software Verification

    Mar 20, 2026Baoding He, Zenan Li, Wei Sun +4Automated Theorem ProvingFormal Verification

    State Key Laboratory of Novel Software Technology, Nanjing University, China · School of Computer Science, Nanjing University, China · Department of Computer Science, ETH Zurich, Switzerland +1

  9. Learning to Disprove: Formal Counterexample Generation with Large Language Models

    Mar 19, 2026Zenan Li, Zhaoyu Li, Kaiyu Yang +2LLM Mathematical ReasoningSynthetic Data Generation for Language Models

    ETH Zurich · University of Toronto · MiroMind +1

  10. Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought

    Mar 18, 2026Zichen Xie, Wenxi WangFormal VerificationLLM Evaluation

    University of Virginia.

  11. Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

    Mar 18, 2026Zenan Li, Ziran Yang, Deyuan He +7Formal VerificationAutomated Theorem Proving

    ETH Zürich · Princeton Language and Intelligence · Department of Computer Science, Princeton University +1

  12. Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents

    Mar 17, 2026Shuvendu K. LahiriAI Agent ReliabilityAutoformalization

    Microsoft Research, USA

  13. Formal verification of tree-based machine learning models for lateral spreading

    Mar 17, 2026Krishna KumarFormal Verification

    aOden Institute of Computational Engineering and Sciences, The University of Texas at Austin, Austin, Texas, USA

  14. From Workflow Automation to Capability Closure: A Formal Framework for Safe and Revenue-Aware Customer Service AI

    Mar 16, 2026Cosimo SperaAI Agent SafetyCustomer Support Automation

    Minerva CQ, 114 Lester Ln, Los Gatos, CA 95032

  15. Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium

    Mar 16, 2026Vasily IlinAutoformalizationFormal Verification

    University of Washington

  16. Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

    Mar 16, 2026Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu +2Fine-TuningTraining Data Curation

    Hebrew University of Jerusalem, Israel · Amherst Col · VMware Research by Broadcom, USA.

  17. Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization

    Mar 16, 2026Banri Yanahama, Akiyoshi SannaiFormal VerificationLean Theorem Proving

    Nyx Foundation · Kyoto University · Large Language Model Research and Development Center, National Institute of Informatics

  18. s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

    Mar 15, 2026Balaji Rao, John Harrison, Soonho Kong +2Automated Theorem ProvingFormal Verification

    Stevens Institute of Technology Hoboken, NJ 07030 · Amazon Web Services Seattle, WA 98101

  19. Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems

    Mar 13, 2026Hongchao Zhang, Mohamad H. Kazma, Meiyi Ma +2Control Barrier FunctionsDynamical Systems

    Department of Computer Science, Vanderbilt University, Nashville, TN 37235 USA. · Department of Civil and Environmental Engineering, Vanderbilt University, Nashville, TN 37235 USA.

  20. Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications

    Mar 12, 2026Liao Zhang, Tong Chen, Xiwei Wu +4Formal VerificationAutoformalization

    School of Computer Science, Shanghai Jiao Tong University · Shanghai Innovation Institute · School of Computer Science and Engineering, University of Washington +1

  21. No Certificate for Alignment: Two Independent Impossibilities and the Pareto Frontier of Achievable Safety Guarantees

    Mar 8, 2026Ayushi AgarwalAI AlignmentFormal Verification

    Independent Researcher

  22. COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance

    Mar 8, 2026Dennis GrossInterpretability in RLSafe RL

  23. FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification

    Mar 6, 2026Lily Jiaxin Wan, Chia-Tung Ho, Yunsheng Bai +4Formal VerificationFormal Hardware Verification

    University of Illinois Urbana-Champaign · NVIDIA · University of Maryland, College Park

  24. Lipschitz-Based Robustness Certification Under Floating-Point Execution

    Mar 6, 2026Toby MurrayNeural Network VerificationNeural Network Robustness

    University of Melbourne, Melbourne, Australia

  25. LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning

    Mar 5, 2026Medina Andresel, Cristinel Mateis, Dejan Nickovic +3AutoformalizationLinear Temporal Logic

    AIT Austrian Institute of Technology, Vienna, Austria · Aristotle University of Thessaloniki, Thessaloniki, Greece · Northeatern University, Boston, MA, USA

  26. Agentic AI-based Coverage Closure for Formal Verification

    Mar 3, 2026Sivaram Pothireddypalli, Ashish Raman, Deepak Narayan Gadde +1Formal Hardware VerificationFormal Verification

    Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany

  27. COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management

    Mar 2, 2026Dennis GrossInventory ControlReinforcement Learning

  28. NM-DEKL∞3^3_\infty: A Three-Layer Non-Monotone Evolving Dependent Type Logic

    Mar 2, 2026Peng ChenNonmonotonic ReasoningFormal Verification

  29. Foundation World Models for Agents that Learn, Verify, and Adapt Reliably Beyond Static Environments

    Feb 27, 2026Florent DelgrangeWorld ModelsAI Agent Reliability

    AI Lab, Vrije Universiteit Brussel & Flanders Make Brussels, Belgium

  30. MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering

    Feb 26, 2026Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee +2Formal VerificationFormal Hardware Verification

    Indian Statistical Institute, Kolkata, India · IBM Systems,India · Texas Instruments,India