Formal Methods in Verification

Latest papers

• NNV3: Expanding Neural Network Verification to New Architectures and Domains

  Anne M. Tumlin, Samuel Sasaki, Ben Wooding, Diego Manzanas Lopez, Muhammad Usama Zubair, Navid Hashemi, Hongchao Zhang, Waseem Abbas, Ipek Oguz, Meiyi Ma, Taylor T. Johnson · 25 September 2026

  We present NNV3, the latest version of the Neural Network Verification (NNV) tool, a MATLAB framework for formal verification of deep learning models and learning-enabled cyber-physical systems. Building on the set-based reachability foundation of NNV 1.0 (FFNNs, CNNs, NNCS) and NNV 2.0 (RNNs, SSNNs…

• Towards An LLM-Driven Unified Conversion Framework for BT and FSM in Autonomous Intelligent Systems

  Zhang Qi, Yang Shuo, Zhu Zhengqiu, Zhou Peng, Jiao Peng · 25 September 2026

  Finite state machine (FSM) and behavior trees (BT) are widely adopted behavioral modeling paradigms for autonomous intelligent systems. While functionally equivalent and inter-convertible in principle, existing transformation methods between FSM and BT face major challenges in preserving behavioral …

• From Reasoning Strings to Partial Orders: Verifier-Certified Rule Transport through Quotient Policy Optimization

  Bang Xie, Hao Liu, Zhiyuan Peng, Xin Yin, Chenhao Ying, Yuan Luo, Senjian Zhang, Wei Chen · 24 September 2026

  Many computations admit several valid execution orders because independent subgoals or disjoint state updates can commute. Reinforcement learning with verifiable rewards usually treats each successful trace as a separate token sequence, so serialization choices can be mistaken for logical dependenci…

• Exploring Solver-Level Warmstarting for Neural Network Verification

  Annelot Bosman, Minghao Liu, Marta Kwiatkowska, Holger Hoos, Jan van Rijn · 23 September 2026

  Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, w…

• Compiling Sufficient Governance Context from Declared Losses and Reachable States: Exact Observation-Contract Synthesis with Cardinality and Cost Objectives

  Gaston Besanson · 23 September 2026

  We call the object this paper derives and certifies a minimal sufficient governance context: given a finite reachable-state model, a deterministic declared verdict, and candidate observable attributes, we compute sufficient observation sets, distinguish attributes that are individually indispensable…

• The Refutation Gap: Certifying Both Halves of an Optimality Claim

  Rohan Pandey · 21 September 2026

  Synthesis pipelines increasingly claim not just that a program is correct, but that it is optimal. Such a claim has two halves with radically different verification stories. The upper bound, "a program of size m exists", is witnessed by an artifact that can be re-executed, proved equivalent to its s…

• Efficient Bayes-Adaptive Reinforcement Learning with Temporal Logic Specifications

  Jonathan Hau, Alessandro Abate · 21 September 2026

  We present a novel end-to-end model-based Reinforcement Learning (RL) algorithm for efficient policy synthesis under given Linear Temporal Logic (LTL) specifications (e.g., safety or reachability) in unknown environments. To do so, a Limit-Deterministic B{\"u}chi Automaton (LDBA) representation of t…

• Large Language Models as Falsifiers for Cyber-Physical Systems

  Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak · 18 September 2026

  Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, …

• Real-Time Synthesis of Robust Controlled Invariant Sets for Monotone Systems

  Yasin Sonmez, Mahmoud Khaled, Majid Zamani, Murat Arcak · 15 September 2026

  Safety-critical control of autonomous systems requires formal safety certificates, such as controlled invariant sets, that must be computed online as conditions change. Although standard synthesis algorithms scale poorly with state dimension, monotone dynamical systems with lower-closed safety speci…

• The Future of Safety for SaMD

  Rhea Malhotra, Tanya Sharma, Krisha Patel, Satvika Sharma, Heena Purkait, Mehak Nehal Makhija, Aellison Cassimiro, Everett Hildenbrandt, Palina Tolmach, Jaidev Shastri · 15 September 2026

  An artificial organ carries failure consequences on the scale of an aircraft or a reactor, but the software driving it is rarely held to the same standard. Teams building them rely on testing, which only reaches the failure modes someone thought of in advance. In a pump or controller that runs insid…

• Supermartingale Certificates for Parametric MDPs

  Kaushik Mallik, {\DH}or{\dj}e \v{Z}ikeli\'c · 14 September 2026

  We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent …

• Learning to adapt GR(1) specifications through degradation

  Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel · 14 September 2026

  Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of s…

• Reinforcement Learning with Temporal-Logic-Based Causal Diagrams

  Yash Paliwal, Rajarshi Roy, Jean-Rapha\"el Gaglione, Nasim Baharisangari, Daniel Neider, Xiaoming Duan, Ufuk Topcu, Zhe Xu · 10 September 2026

  We study a class of reinforcement learning (RL) tasks where the objective of the agent is to accomplish temporally extended goals. In this setting, a common approach is to represent the tasks as deterministic finite automata (DFA) and integrate them into the state-space for RL algorithms. However, w…

• No Free Checker: A Survey of Verifiers for Robot Policies

  Yang Wan, Xihang Yue, Zhirui Liu, Ziyuan Chu, Shuxun Wang, Yuhan Chen, Xiaonan Jiang, Xukun Zhu, Yubo Dong, Linchao Zhu · 10 September 2026

  A verifier for robot policies reads a candidate behavior and returns a score for how well it did, used both to evaluate vision-language-action policies and to train them. Verifiers range from success detectors and reward models to runtime monitors, safety filters, and temporal-logic specifications. …

• Application of curiosity driven exploration methods for hardware interference identification

  Ludovic Matar, Clement Moulin-Frier, Pierre-Yves Oudeyer · 9 September 2026

  The transition from single-core to multi-core architectures in safety-critical embedded systems introduces significant challenges due to inter-core interference caused by contention for shared hardware resources. Such interference affects execution times and complicates the verification of strict te…

• Generator-Independent Runtime Assurance under Partial Observation

  Guangxi Wan, Yongbo Xie, Yuqi Liu, Qingwei Dong, Qingxin Li, Hongfei Bai, Peng Zeng · 9 September 2026

  Proposal-based controllers---learned policies, language-model planners, and other black-box \emph{generators}---are increasingly deployed behind runtime verification gates. We ask when the closed-loop safety guarantee decouples from the generator. The prevailing per-candidate certification pattern d…

• SiLR: Structure-Preserving Admission and Process Reward for LLM Tool Agents

  Chenyu Zhou, Qiliang Jiang, Shuning Wu, Xu Zhou · 7 September 2026

  A runtime gate for an LLM tool agent is usually cast as a filter. In a ReAct loop a rejected proposal is followed by another at the same state, so the gate is a search operator over the proposal stream whose admission criterion shapes which trajectories are reachable. We study post-violation recover…

• On Synthesis of Metric Interval Temporal Logics

  Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj Madnani · 2 September 2026

  Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to ta…

• Probabilistic Model Checking of Autoregressive Neural Sequence Models

  Helge Spieker, Dennis Gross, Arnaud Gotlieb · 2 September 2026

  Test-set accuracy is silent on two issues that matter when deploying autoregressive neural sequence models: how much probability mass the system under test (SUT) places on constraint-violating alternatives that are reachable under sampling and what fraction of the input population satisfies a domain…

• PanelShield: Verifiable Closed-Loop Safe Planning for Robotic Industrial Panel Operation

  Guipeng Xin, Jiahe Xu, Chenhui Wan, Jie Liu, Youmin Hu, Zhongxu Hu · 31 August 2026

  Industrial panel operation is knowledge-intensive and safety-critical. Beyond control recognition and action generation, execution must satisfy constraints in operation manuals and safety regulations. While foundation-model-based planners show strong semantic capability, they typically lack computab…

• Categorizer Automata for Discounted-Sum Payoffs

  Nathalie Bertrand, Pranav Ghorpade, Senthil Rajasekaran, Sasha Rubin, Moshe Vardi · 28 August 2026

  Categorizing continuous data into discrete bins is a fundamental operation in artificial intelligence. We introduce the categorizer automaton, a deterministic automaton that reads an infinite sequence of rewards and identifies which of finitely many bins contains its discounted sum. Categorizer auto…

• Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

  Zhiyuan Yan, Ziyue Zheng, Hongce Zhang · 20 August 2026

  Hardware functional verification relies on high-quality assertions to expose design bugs and establish confidence in Register Transfer Level (RTL) designs. Yet existing assertion mining methods still struggle to produce complete and reliable assertion sets: random or limited traces fail to cover har…

• An Omitted Mode Is a Rare Rule: The Sampling-Verification Danger Law in Continuous Code World Models

  Javier Aguilar Martín · 19 August 2026

  In the Code World Model paradigm an LLM synthesizes an executable world model that a classical planner searches, and the model is accepted when it reproduces sampled transitions. We ask what that acceptance certifies in continuous control. We define the pipeline's danger as an expected risk and isol…

• Backward through Time, Algebraically

  Konstantinos Kogkalidis · 19 August 2026

  Linear temporal logic is a modal extension of propositional logic that allows one to state how a system should behave over time. Its canonical domain is the booleans, but discretely-valued judgements are of little use in steering softly-valued systems (neural policies, adaptive controllers, sequence…

• Temporal Logic Guided Universal Task Representations for Reinforcement Learning

  Hao Zhang, Zhangli Zhou, Zhen Kan · 18 August 2026

  Task guided agents demonstrate strong performance in a wide range of complex tasks. However, most existing task representation algorithms are tailored to specific contexts and struggle to generalize across diverse scenarios. Moreover, they typically depend on gradient signals from reinforcement lear…