The TLA ^+ language has been widely used, both in academia and industry, to specify and reason about distributed systems. This paper presents Apalache, an efficient and flexible symbolic model checker for TLA ^+ . Apalache’s engine is based on bounded model checking, with symbolic transitions being extracted from TLA ^+ specifications and verification conditions suitable for satisfiability modulo theories (SMT) solvers being generated from them. Reasoning can be done in terms of safety and liveness properties, with liveness checking realised via a liveness-to-safety reduction. Apalache’s flexibility lies in its three complementary functionalities: bounded exhaustive verification, for bounded guarantees, randomised symbolic execution, for prototyping and bug detection, and inductiveness checking, for unbounded guarantees. The paper describes Apalache’s architecture and features, including its support for PlusCal and Quint, two languages that share the same semantic foundation as TLA ^+ . Industrial usage of Apalache is also presented, together with a case study which illustrates how Apalache can be used to verify the agreement property of a consensus protocol.
Burrow is a proof framework for weak memory mapping proofs. Those mappings appear as optimizations and translations between languages inside compilers and binary translators. However, their mechanized proofs, when defined over formal axiomatic weak memory semantics, are often large and complex. In this paper, we discuss the proof primitives provided by Burrow which simplify mechanizing those mapping proofs and help to prove many lemmas generally. To demonstrate the benefits of these primitives, we use Burrow to prove a mapping from x86 to Arm correct.
A DFA separates two disjoint languages L_1 and L_2 if it accepts every word in L_1 and rejects every word in L_2. Algorithms for active learning of small separating DFAs have many applications, e.g., for learning network invariants, learning contextual assumptions in compositional verification, learning state machines from large amounts of log data, and learning bug pattern descriptions. We propose a simple active learning algorithm, inspired by L^#, that learns a minimal separating DFA for disjoint languages L_1 and L_2 if one exists. Experiments show that our algorithm significantly outperforms existing active learning algorithms on both randomly generated and industrial benchmarks.
We study the problem of generating paths on a graph that satisfy a collection of ω -regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of ω -regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.
Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak ω-automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation and synthesis.
We consider the use of commutativity-based reduction for the algorithmic verification of concurrent programs. In existing work, the commutativity relation used for the reduction is mostly fixed statically. In this paper, we propose a demand-driven approach to compute the commutativity relation. The approach can be viewed as the direct analogue of the CEGAR approach which uses counterexamples to guide the incremental refinement of the abstraction. Instead of eliminating a counterexample by proving it infeasible and refining the abstraction, we can eliminate a counterexample by proving it redundant and expanding the commutativity relation. When we prove a counterexample redundant, we use the proof for a generalization step which allows us to eliminate not just a single counterexample, but a whole infinite set. We present a general scheme where we integrate the new approach with the CEGAR approach. We have implemented an instantiation of the general scheme. An experimental evaluation shows an increase in the number of successfully verified programs by 15% on a challenging benchmark set.
We present Sprout, the first sound and complete implementability checker for symbolic multiparty protocols. Sprout supports protocols with dependent refinements on message values, loop memory, and multiparty communication with generalized, sender-driven choice. Sprout checks implementability via an optimized, sound and complete reduction to the fixpoint logic μ CLP, and uses MuVal as a backend solver for μ CLP instances. We evaluate Sprout on an extended benchmark suite of implementable and non-implementable examples, and show that Sprout outperforms its competititors in terms of expressivity and precision, and provides competitive runtime performance. Sprout additionally provides support for verifying custom functional correctness properties beyond implementability.
Runtime enforcers receive events from a system and output commands ensuring the system's policy compliance. Proactive enforcers extend traditional (reactive) enforcers by emitting commands at any time, rather only as a response to system actions. However, proactive enforcers have so far lacked support for many useful policy features. This, along with the existing tools' poor performance, hinders their adoption. We present a performance-optimized, proactive enforcement algorithm for a rich policy language: metric first-order temporal logic with function applications, aggregations, and let bindings. We have implemented this algorithm in ENFGUARD, the first proactive enforcer tool that supports the above constructs. We evaluated our tool using a novel set of six benchmarks containing both real-world and synthetic policies and logs, demonstrating that it enforces realistic policies out-of-the-box and achieves the necessary performance to be used in real-time systems.
We present Veil, an open-source framework for automated and interactive verification of transition systems, aimed specifically at conducting machine-assisted proofs about concurrent and distributed algorithms. Veil is implemented on top of the Lean proof assistant. It allows one to describe a transition system and its specification in a simple imperative language, producing verification conditions in first-order logic, to be discharged automatically via a range of SMT solvers. In case automated verification fails or if the system's description requires statements in a higher-order logic, Veil provides an interactive verification mode, by virtue of being embedded in a general-purpose proof assistant. We have evaluated Veil on a large set of case studies from the distributed system verification literature, showing that its automated verification performance is acceptable for practical verification tasks, while it also allows for seamless automated/interactive verification of system specifications beyond the reach of existing automated provers.
We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars in the style of Courcelle. Due to the undecidability of verification problems such as reachability or coverability of a given configuration, in which we count the number of replicas in each local state, we develop two orthogonal verification techniques. We present a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets that over-approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evaluated on a non-trivial set of test cases. Moreover, we identify a decidable fragment, for which the coverability problem is in 2EXPTIME and PSPACE-hard.
This paper presents StarV, a new tool for verifying deep neural networks (DNNs) and learning-enabled Cyber-Physical Systems (LeCPS) using the well-known star reachability. Distinguished from existing star-based verification tools such as NNV and NNENUM and others, StarV not only offers qualitative verification techniques using Star and ImageStar reachability analysis but is also the first tool to propose using ProbStar reachability for quantitative verification of DNNs with piecewise linear activation functions and Le-CPS. Notably, it introduces a novel ProbStar Temporal Logic formalism and associated algorithms, enabling the quantitative verification of DNNs and Le-CPS's temporal behaviors. Additionally, StarV presents a novel SparseImageStar set representation and associated reachability algorithm that allows users to verify deep convolutional neural networks and semantic segmentation networks with more memory efficiency. StarV is evaluated in comparison with state-of-the-art in many challenging benchmarks. The experiments show that StarV outperforms existing tools in many aspects, such as timing performance, scalability, and memory consumption.
We introduce QSM-Cutoff, a new procedure that employs the quantified symmetric minimization algorithm from [12] to systematically derive quantified formulas that precisely capture the onset of cutoff and saturation in distributed protocols. QSM-Cutoff performs symmetry-aware forward reachability to enumerate the reachable states of a finite protocol instance, and applies symmetry-preserving logic minimization to express these states as a minimum-cost finitely-quantified reachability formula. QSM-Cutoff repeats this finite analysis process to derive a sequence of reachability formulas R_1, R_2, R_3, ⋯ at increasing protocol sizes. This process terminates at size k when R_k is a unique solution to symmetric minimization that yields the exact set of reachable states when evaluated at size k+1 . We define c :=k as the cutoff size and R_c:=R_k as the cutoff formula. Empirically, R_c is shown to be a reachability invariant that encodes the reachable states for any protocol size. QSM-Cutoff extends the finite analysis process in [12] by introducing two algorithmic enhancements: a depth-first search algorithm that enumerates the reachable states of a finite protocol by searching only for their symmetric quotient, and an extended quantification pattern inference algorithm that expresses explicit clause orbits of finite instances by logically equivalent quantified formulas. Empirical results demonstrate that, compared to the techniques used in [12], QSM-Cutoff is able to analyze a larger corpus of protocols, derive more compact quantified inductive invariants, and converge at smaller cutoffs. In contrast to previous scholarship, QSM-Cutoff offers a new angle for understanding the notions of cutoff and saturation of distributed protocols. In particular, it raises intriguing questions about the unexpected role of symmetric logic minimization in this much-researched area and opens new directions for further research.
This paper presents a modular approach to verifying the vector module of PETSc, a widely used library in scientific computing, using the CIVL model checker. Our approach relies on the creation of stub functions, which serve a dual purpose of specifying the intended behavior of individual PETSc functions and providing an abstraction for called functions to allow efficient verification of callers. This facilitates the use of symbolic execution and model checking to establish the correctness of isolated functions. Our work contributes to the ongoing effort to enhance the reliability of high-performance computing libraries and proposes an effective verification strategy for complex scientific software.
Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness generator) and the corresponding arithmetic circuits, from which the prover and verifier can be automatically generated. However, for these programs to be correct, the witness generator and the arithmetic circuit need to be mutually consistent in a certain technical sense, and inconsistencies can result in security vulnerabilities. This paper formalizes the consistency requirement for circuit DSLs and proposes the first automated technique for verifying it. We evaluate the method on hundreds of real-world circuits, demonstrating its utility for both automated verification and uncovering errors that existing tools are unable to detect.
Knowledge compilation (KC) involves compiling propositional constraints into tractable target languages which in turn efficiently support multiple analyses or queries of the constraints. Solving these queries plays a crucial role in the synthesis and verification of hardware and software systems. Recently, we proposed the target language, Constrained Conjunction Decision Diagrams (CCDD), experimentally shown to be promising for individual model counting queries. Here, we present the compiler, , which compiles CNF into CCDD. supports a range of queries. We present an empirical evaluation focusing on two fundamental queries, uniform sampling and (multiple) model counting, with a wide range of applications. While counting and sampling have witnessed significant performance improvements over the years, scalability still remains the primary challenge. Our evaluation over 600 instances from model counting competitions 2022–2024 show that achieves state of art compilation by solving 322 instances, which is 183, 148, and 38 more than Dsharp, miniC2D, and D4 respectively. Secondly, on repetitive tasks, solves 53 and 50 more instances than ExactMC and SharpSAT-TD for model counting, and 175 and 132 more instances than SPUR and KUS for uniform sampling, respectively.
Automated program verifiers such as Dafny, F ^⋆ , Verus, and Viper are now routinely used to verify real-world software. Unfortunately, the performance of the SMT solvers employed by these tools is not always able to keep up with the increasing size and complexity of verification problems, resulting in long verification times and verification failures due to time-outs. This performance degradation occurs because large SMT queries increase the search space for the SMT solver, in particular, the number of possible quantifier instantiations. Most existing attempts to mitigate this problem require substantial manual effort to reduce the size of the search space, for instance, by decomposing proofs. In this paper, we present an automatic technique to significantly improve the performance of SMT-based program proofs by drastically reducing the proof search space for each assertion, in particular, the performed quantifier instantiations. Starting from a successful verification, we automatically extract for each assertion the quantified axioms used by the SMT solver to show that the assertion is valid. Crucially, these include lurking axioms, which are logically irrelevant, but needed to trigger the instantiation of other, relevant axioms. We describe a novel proof localization algorithm that implements a semantics-preserving source-to-source translation of a program such that re-verifying an assertion in the optimized program uses only the axioms in its proof essence. This rewriting greatly reduces the possible quantifier instantiations and, thereby, the search space for the SMT solver, such that all future runs of the verifier, for instance as part of continuous integration, are substantially faster. We implemented our algorithm for the Boogie verifier and demonstrated its effectiveness on examples from Dafny and Viper. Specifically, for files with verification times over a minute, we show significant speedups of up to 100–1000 times and no slowdowns. We also provide some evidence that these improvements persist as projects evolve.
We develop decision procedures for extended regular expressions in the new ERE framework that uses span semantics, utilizing the power of symbolic derivatives. We prove a normal form theorem in Lean for ERE that is closed under all Boolean operations and provides the basis for the given decision procedures. The tool is evaluated on existing SMT benchmarks for regexes that shows it to be the fastest solver to date – often orders of magnitude faster than state-of-the-art – albeit specialized for the single-variable fragment of string theory.
rlive is a recently-proposed SAT-based liveness model checking algorithm that showed remarkable performance compared to other state-of-the-art approaches, both in absolute terms (solving more problems overall than other engines on standard benchmark sets) as well as in relative terms (solving several problems that none of the other engines could solve). rlive proves or disproves properties of the form FGq, by trying to show that ¬ q can be visited only a finite number of times via an incremental reduction to a sequence of reachability queries. A key factor in the good performance of rlive is the extraction of “shoals” from the inductive invariants of the reachability queries to block states that can reach ¬ q a bounded number of times. In this paper, we generalize rlive to handle infinite-state systems, using the Verification Modulo Theories paradigm. In contrast to the finite-state case, liveness cannot be simply reduced to finding a bound on the number of occurrences of ¬ q on paths. We propose therefore a solution leveraging predicate abstraction and termination techniques based on well-founded relations. In particular, we show how we can extract shoals that take into account the well-founded relations. We implemented the technique on top of the open source VMT engine IC3ia and we experimentally demonstrate how the new extension maintains the performance advantages (both absolute and relative) of the original rlive, thus significantly contributing to advancing the state of the art of infinite-state liveness verification.
The design of computer microarchitectures is a challenging task, involving a trade-off between efficiency and security. In the literature, two concerns which are affected by the details of the microarchitecture – formal assembly semantics, and vulnerability discovery and mitigation – are often addressed separately. In this paper we provide a structural operational semantics for pipelined microprocessors (Arm, x86, RISC-V) that is based on a regular understanding of microarchitectural features (pipelines, branch prediction, caches, privilege checks), conforms to established memory consistency models, and exposes the Spectre and Meltdown vulnerabilities. A key point is that the operational rules correspond to stages of the pipeline and are based almost entirely on syntactic aspects of fetched instructions, as is generally understood to be the case in real pipelines. We develop a model checker based closely on the semantics, which we use to experimentally validate the model and to provide the basis for security analyses.
Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic. Viper consists of the Viper intermediate language and two backend verifiers based on symbolic execution and verification condition generation, respectively. It has been used to build over a dozen program verifiers that translate verification problems in Go, Java, Python, Rust, and many others, into the Viper language and automate verification using the Viper backends. In this paper, we describe the original design goals for Viper's language, verification logic, and tool architecture, summarize our experiences, and explain our principles for evolving the system.
