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. Composing Verifiable Conceptual Models via Building Blocks: Towards Design-Time Verification of Agentic AI Workflows

    Jun 19, 2026Noe Y. Flandre, Alexander C. Nwala, Philippe J. GiabbanelliAgentic WorkflowsFormal Verification

  2. Temporal logics and formal synthesis for robot planning and control

    Jun 19, 2026Jana Tumova, Joris Verhagen, Matti VahsRobotic ControlSignal Temporal Logic

  3. AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

    Jun 18, 2026Han Zhou, Yu Luo, Dianxiang XuFormal Verification

  4. A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA

    Jun 18, 2026Raik Hipler, Martin Leucker, Patrick RodlerFormal VerificationFault Localization

  5. Analyzing the Narration Gap in LLM-Solver Loops

    Jun 17, 2026Zunchen Huang, Songgaojun DengAdversarial Attacks on LLMsFormal Verification

  6. ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

    Jun 17, 2026Pierre Dantas, Lucas Cordeiro, Waldir JuniorFormal Verification

  7. As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture

    Jun 16, 2026Marcos Abel Zuzuárregui, Stefano CarpinLarge Language Model-Based Robot PlanningFormal Verification

  8. IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

    Jun 16, 2026Elliot Jones, William KnottenbeltAutomated Theorem ProvingFormal Verification

  9. A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics

    Jun 16, 2026Marco Aruta, Vadim Malvone, Aniello Murano +2Formal VerificationMulti-Agent Systems

  10. TNODEV: Toolbox for Neural ODE Verification

    Jun 15, 2026Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed GhazelNeural Network VerificationReachability Analysis

  11. The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

    Jun 15, 2026Noor Islam S. Mohammad, Tamim SheikhFormal VerificationLean Theorem Proving

  12. Theorem-Grounded Execution Ontologies for Interpretable Machine Reasoning

    Jun 14, 2026Raghu AnantharangacharInterpretable MLFormal Verification

  13. ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

    Jun 13, 2026Pierre Dantas, Lucas Cordeiro, Waldir JuniorSafety-Critical ControlFormal Verification

  14. VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization

    Jun 13, 2026Zhixin Hu, Tao Xu, Xiaodian Sun +2Automated Theorem ProvingFormal Verification

  15. A Formal Tool for Verification of Probabilistic Spiking Neural Networks Based on Quotient Abstractions

    Jun 12, 2026Nikan Zandian Jazi, Elisabetta De Maria, Christopher LeturcNeural Network VerificationFormal Verification

  16. Contract-Based Compositional Shielding for Safe Multi-Agent Reinforcement Learning

    Jun 12, 2026Omar Adalat, Edwin Hamel-De le Court, Francesco BelardinelliMulti-Agent CoordinationFormal Verification

  17. Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

    Jun 11, 2026Vasily Ilin, Brian NugentFormal VerificationLean Theorem Proving

  18. Shielded Analysis: Certification and Characterization of Defensibility in Systems under Adversarial Interaction

    Jun 11, 2026Achraf Hsain, Sultan AlmuhammadiAutonomous Cyber DefenseAdversarial Robustness

  19. TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

    Jun 4, 2026Eric Spencer, Arslan Bisharat, Brian Ortiz +6LLM-Based Program SynthesisFormal Verification

  20. Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

    Jun 4, 2026Arslan Bisharat, Brian Ortiz, Eric Spencer +5LLM EvaluationFormal Verification

  21. VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents

    Jun 3, 2026Yunhao Yang, Neel P. Bhatt, Kevin Wang +3Robot Skill LearningLarge Language Model-Based Robot Planning

  22. CARVE-Q: Quantum-Proposed, Classically Certified Interactive Driving Repair

    Jun 3, 2026Yifan WangFormal VerificationAutonomous Driving Planning

  23. Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

    Jun 2, 2026Ruida Wang, Jerry Huang, Pengcheng Wang +3Software Engineering AgentsFormal Verification

  24. Glass Box at Orbit: A Constitutional AI Verification Framework for Trustworthy Autonomous CubeSat Intelligence

    Jun 2, 2026Karthik Barma, Anil Sanneboyina, V C Premchand YadavAI AlignmentAI Agent Safety

  25. CARVE: Certified Affordable Repair of Vetoed Maneuvers via Envelopes for Interactive Driving

    May 31, 2026Yifan WangFormal VerificationAutonomous Driving Planning

  26. FVSpec: Real-World Property-Based Tests as Lean Challenges

    May 31, 2026Quinn Dougherty, Max von Hippel, Simon Henniger +2Automated Software TestingAutomated Theorem Proving

  27. Robust Shielding for Safe Reinforcement Learning

    May 29, 2026Edwin Hamel-De le Court, Thom Badings, Alessandro Abate +2Robust Markov Decision ProcessesFormal Verification