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. EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming

    Aug 3, 2026Kaustuv Mukherji, Jaikrishna Manojkumar Patil, Colton Payne +4Logic ProgrammingSoftware Vulnerability Detection

    Syracuse University · HRL Laboratories

  2. Alternating-Time Temporal Logic with Mean-Payoff Guarantees

    Aug 2, 2026Muhammad NajibGame TheoryFormal Verification

    Heriot-Watt University, Edinburgh, UK

  3. Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety

    Aug 2, 2026Ruiyang ZhangFormal VerificationAI Agent Monitoring

    Ryonix Labs Inc. Flock.io

  4. An AI Approach to Verified Production Cryptographic Libraries

    Aug 2, 2026Chuyue Sun, Su Fong, Zhiyi Kuang +5Software SecurityProgram Synthesis

    Stanford University · &Truth · University of North Carolina at Chapel Hill +2

  5. Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

    Aug 1, 2026David A. NaumannLogical ReasoningFormal Verification

    Stevens Institute of Technology, USA

  6. Verifiable Checks for Business Rule Consistency

    Aug 1, 2026Joseph Tafese, Milad Hooshyar, Sam Bayless +2Formal Verification

    University of Waterloo · Waterloo, Canada · Amazon +1

  7. Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains (Extended Version)

    Aug 1, 2026Jianlin Li, Nick Guo, Peter Ye +1Reachability AnalysisMarkov Models

    David R. Cheriton School of Computer Science University of Waterloo, Canada

  8. Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

    Jul 30, 2026Ha Trung TranFormal Hardware VerificationAutomated Program Repair

    Independent Researcher · Seattle, WA, USA

  9. LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean

    Jul 30, 2026Pablo Manrique, Stefan SzeiderSymmetry BreakingFormal Verification

    Algorithms and Complexity Group TU Wien, Vienna, Austria

  10. WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization

    Jul 30, 2026Fanzhe Wei, Li Liu, Ziyang Wang +1KV CachingMemory-Efficient Inference

    Metask Lab

  11. Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models

    Jul 30, 2026Yang Li, Ping Hou, Nobuko YoshidaLLM-Based Program SynthesisFormal Verification

    University of Oxford Computer Science Oxford, United Kingdom

  12. VeriSkill: A Self-Evolution Framework for Program Verification Skills

    Jul 30, 2026Changguo Jia, Tianqi Zhao, Zhiyou Xiao +2LLM Agent Self-ImprovementFormal Verification

    Peking University, Beijing, China · Zhongguancun Laboratory, Beijing, China · Shanghai Jiao Tong University, Shanghai, China

  13. Specula: Scaling formal specifications for autonomous model checking of system code

    Jul 28, 2026Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang +6Software Engineering AgentsFormal Verification

    Nanjing University Nanjing, China · University of Illinois Urbana-Champaign, IL, USA · Microsoft Research Asia Beijing, China +1

  14. PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering

    Jul 26, 2026Dongxu Yang, Ziyi LiangKG ConstructionSpatiotemporal Reasoning

    DeepLethe

  15. Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL

    Jul 26, 2026Shuqing ZhaoFormal Hardware VerificationFormal Verification

  16. Formalizing Flag Algebras in Lean

    Jul 26, 2026Gyeongwon Jeong, Seonghun Park, Jihoon Hyun +2Formal Verification

    School of Computing, KAIST, Daejeon, Korea · School of Computational Sciences, Korea Institute for Advanced Study (KIAS), Seoul, Korea · Discrete Mathematics Group, Institute for Basic Science (IBS), Daejeon, Korea +1

  17. TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation

    Jul 26, 2026Arslan Bisharat, Eric Spencer, Brian Ortiz +8LLM EvaluationFormal Verification

    Loyola University Chicago Chicago, Illinois, USA

  18. Emergent Behaviour in Financial Markets

    Jul 25, 2026Omar Inverso, Emilio Tuosto, Dragisa ZunicFormal VerificationFinance

    Gran Sasso Science Institute, Italy

  19. CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference

    Jul 24, 2026Jiyuan Tan, Vasilis SyrgkanisAI Agents for Scientific DiscoveryAutomated Theorem Proving

  20. Towards a Certifying Grounder

    Jul 23, 2026Daimy Van Caudenberg, Alexander Ek, Carlos Cantero +1Formal Verification

    KU Leuven, Leuven, Belgium · ARC Training Centre OPTIMA, Melbourne, Australia · Vrije Universiteit Brussel, Brussels, Belgium

  21. Animation, Verification and Visualisation of Prolog Transition Systems with ProB

    Jul 23, 2026Jan Gruteser, Michael Leuschel, Katharina Engels +1Logic ProgrammingFormal Verification

    Heinrich Heine University Düsseldorf · Faculty of Mathematics and Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universitätsstr. 1, D-40225 Düsseldorf

  22. Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB

    Jul 23, 2026Katharina Engels, Jan Gruteser, Michael LeuschelAutomated Theorem ProvingInteractive Theorem Proving

    Heinrich Heine University Düsseldorf · Faculty of Mathematics and Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universitätsstr. 1, D-40225 Düsseldorf

  23. Evaluating Large Language Models for Symbolic Security Protocol Analysis

    Jul 22, 2026Paolo Modesti, Syed Ahmed, Ioannis Sfyrakis +1LLM EvaluationCybersecurity

    Teesside University, Middlesbrough, United Kingdom

  24. Lookahead Branching for Neural Network Verification

    Jul 19, 2026Liam Davis, Duo Zhou, Huan Zhang +3Neural Network VerificationBranch and Bound

    Amherst College · University of Illinois Urbana-Champaign · Hebrew University of Jerusalem +1

  25. Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits

    Jul 18, 2026Haifeng Li, Mo HaiMetamorphic TestingFormal Verification

    School of Information, Central University of Finance and Economics

  26. SMC-ES: Automated synthesis of formally verified control policies

    Jul 16, 2026Riccardo Curcio, Toni Mancini, Enrico TronciFormal VerificationSafe RL

    Department of Computer Science, Sapienza University of Rome, via Salaria 113, 00198 Rome, Italy

  27. The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK

    Jul 15, 2026Tobias PhilippAI Coding AgentsCode Generation

    secunet Security Networks AG, Essen, Germany

  28. Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs

    Jul 14, 2026Junyu RenLLM Hallucination MitigationEvidence-Grounded Reasoning

    Committee on Computational and Applied Mathematics, University of Chicago, Chicago, IL, USA.

  29. Learning Linear Temporal Specifications from Demonstrations with Uncertainty

    Jul 12, 2026Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oesFormal VerificationLearning from Demonstration

    School of Electrical Engineering and Computer Science at The Pennsylvania State University, State College, USA

  30. Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

    Jul 11, 2026Yiannis Charalambous, Rafael Menezes, Youcheng Sun +1Formal Verification

    The University of Manchester