ABSTRACT. Single Sign-On (SSO) protocols allow an identity provider to authenticate users and report the outcome by issuing identity attestations. Recent attacks show that breaching the identity provider infrastructure enables adversaries to issue arbitrary identity attestations and impersonate users. Survivable SSO protocols limit the risks of similar intrusions, but they have only been defined for password-based authentication, inheriting their limitations against powerful attacks such as credential phishing. While phishing-resistant passwordless authentication protocols have been standardized, they are not designed to guarantee intrusion tolerance. We initiate the research for Survivable Passwordless SSO (SPS) and propose a modular approach which includes the novel definition of Survivable Passwordless Challenge-response (SPC) protocols for authentication as a sub-routine of SSO. We give the first frameworks and game-based security definitions both for SPC and SPS which capture both novel attack classes, such as session injection attacks in a decentralized setting, and existing but not yet formalized attack classes, such as detection of cloned authenticators. The design of the models includes novel strategies to capture proactive security in survivable protocols within security definitions and to compose authentication and SSO through a modular approach. Our strategies and models may also be applied with minor modifications to non-survivable protocols, possibly providing a novel approach to assess the security of existing SSO protocols.

ABSTRACT. This paper presents a formal framework for enhancing privacy in decentralized identity (DID) systems, resolving the inherent conflict between blockchain verifiability and the principle of minimal data disclosure. At its core, we introduce a provably secure cryptographic protocol that leverages attribute commitments on-chain and zero-knowledge proofs for off-chain validation. This approach allows users to demonstrably prove the validity of predicates about their attributes without revealing the underlying sensitive values. We formally define the security and privacy requirements for such a system—including consistency, attribute-based indistinguishability, and predicate-based indistinguishability—within a semi-honest adversarial model. We then construct a concrete scheme that realizes these properties under standard cryptographic assumptions. The proposed architecture is designed for full backward compatibility with W3C DID standards, ensuring practical deployability. Security analysis provides rigorous, provable guarantees, while performance evaluation confirms the efficiency of the core cryptographic operations, supporting its use in resource-constrained environments. This work establishes a foundational and analyzable basis for building decentralized identity systems where both accountability and user privacy are essential.

ABSTRACT. Existing Capture-the-Flag (CTF) platforms trust a single organizer, offer limited auditability, and are vulnerable to infrastructure-level manipulation. We propose zk–MPSFV, a zk-SNARK-based, multi-phase sub-flag verification scheme that replaces centralized scoring with an on-chain, zero-knowledge, publicly verifiable scoreboard. Challenges are decomposed into sub-challenges arranged as a directed acyclic graph (DAG): a team unlocks the next step only after proving completion of all parent nodes. Sub-flags and decryption keys are jointly generated by n organizers and released via an off-chain (t, n) Shamir–BLS threshold signature produced through multi-party computation (MPC), preventing any single organizer from leaking or altering keys. Teams submit zk-PLONK proofs that the contract verifies, timestamps, and records immutably. Under standard assumptions (collision-resistant hashing, SNARK soundness/zero-knowledge, IND-CCA2 ECIES, and at least t honest organizers), we prove that zk–MPSFV achieves the stated security goals, including DAG-gated progress, anti-replay, and threshold-robust organizer security, while out-of-band flag sharing remains out of scope. On a three-organizer testbed with 30 simulated teams, setup costs 0.45 ms per sub-flag, proof generation averages 5.34 s on an 8-core system, and on-chain verification costs ≈ 170k L2 gas on zkSync Era with a median fee of 1.33×10−6 ETH (about $0.0046 at $3,435/ETH). Stress replays sustain ≈ 7 proof transactions/s up to 5000 proofs; extrapolating to 50,000 proofs (1000 teams× 50 submissions) yields ≈ 0.0665 ETH (about $200–$228) and ≈ 2 hours of settlement time. Overall, zk–MPSFV is practical for small- to mid-scale, audit-ready progression CTFs.

ABSTRACT. Consistency-based diagnosis is a formal approach to software fault localization that explains failing executions by identifying program components whose modification would restore correctness. Tools such as BugAssist and (more recently) CFaults instantiate this idea using logical encodings and bounded model checking. In our first contribution, we improve on this line of work. We present SherLoc, a consistency-based diagnosis engine for ANSI-C programs with multiple failing test cases. SherLoc introduces an explicit repair model that supports pointers and arrays, ensuring that diagnoses correspond only to semantically valid C repairs. In addition, we adapt efficient algorithms from hardware diagnosis, which avoid costly self-composition, and significantly outperform existing tools on standard benchmarks. In our second contribution, we expose fundamental limitations of formal fault localization: program optimizations and transformations can invalidate diagnoses despite semantic equivalence, representing a major hurdle to further scalability improvements; function inlining can break the functional consistency of repairs, yielding diagnoses that cannot be realized at the source level; and bounded encodings inherently miss diagnoses in the presence of loops or unbounded behavior. Our exposition clarifies the gap between the formal ideal of sound and complete diagnosis and what current techniques can realistically guarantee, and thereby helps guide future work toward more robust and principled approaches.

ABSTRACT. We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto industrial C++ codebases where correctness arguments are embedded within implementation artifacts. We focus on a formal analysis of the core SDEX algorithm which implements the Stellar blockchain’s order-book. By combining Large Language Models, the Prototype Verification System (PVS) and Seahorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of interactive theorem proving and model checking provides a path for delivering actionable assurance to legacy, high-value systems.

ABSTRACT. SvLibChecker is a small tool for software model checking. The goal of the tool is to provide a light-weight framework that makes it easy to implement and explore algorithms for verifying software. The input to SvLibChecker is given in SV-LIB, an intermediate language that relieves the developers from dealing with sophisticated language features and their semantics. Software verifiers can normally be complex software systems with hundreds of thousands of lines of code. Due to the simple input, algorithms in SvLibChecker can be written in a succinct way. Our tool currently provides six different model-checking algorithms. Each algorithm consists of about 100 lines of Python code. The full project has about 2500 LOC in total, which are well-documented and have a good test coverage (> 90 %). The simplicity, lean architecture, and modular design of SvLibChecker lends itself for education. It is much easier to understand the implementation of an algorithm implemented in SvLibChecker, compared to complex verifiers for languages like C. SvLibChecker’s predicate abstraction with CEGAR has a performance comparable to CPAchecker, a mature state-of-the-art tool for software verification. The combination of simplicity and performance makes SvLibChecker a suitable tool for verification researchers and educators, for experimenting with new verification approaches and teaching students.

ABSTRACT. We present PyCHC, a solver-agnostic framework aimed at systems of constrained Horn clauses (CHC). PyCHC provides intuitive Python APIs to create and manipulate CHC systems programmatically and solve them using different backend solvers. Furthermore, PyCHC offers a certification pipeline to validate the correctness of results reported by the CHC solvers, via the use of independent satisfiability modulo theories (SMT) solvers and proof checkers. We present our framework's architecture and features, and demonstrate how it enables rapid prototyping of new CHC-based algorithms and experimentation with novel strategies for cooperative solving. We used PyCHC to validate the results of the Eldarica, Golem, and Spacer solvers on CHC-COMP benchmarks, finding several issues across different tool versions.

ABSTRACT. Attack trees (ATs) are popular graphical models for reasoning about the security of complex systems, allowing for the quantification of risk through so-called AT metrics. A large variety of different such AT metrics have been proposed, and despite their wide-spread practical use, no systematic treatment of attack tree metrics so far is fully satisfactory. Existing approaches either fail to include important metrics, or they are too general to provide a useful systematic way for defining concrete AT metrics, giving only an abstract characterisation of their behaviour. We solve this problem by developing a compositional theory of ATs and their functorial semantics based on gs-monoidal categories. Viewing attack trees as string diagrams, we show that components of ATs form a channel category, a particular type of gs-monoidal category. AT metrics then correspond to functors of channel categories. This characterisation is both general enough to include all common AT metrics, and concrete enough to define AT metrics by their logical structure.

ABSTRACT. Active cyber defense offers a promising approach to addressing the longstanding asymmetry between rapidly evolving cyber threats and static defense systems. However, active cyber defense requires fast responses and proactive reconfigurations that must be verified and tailored to observed attacker be- haviour. Formal methods rely on rigorous mathematical and logical frameworks for verifying system specifications under well- defined assumptions. In particular, multi-agent system (MAS) verification, which examines formal properties of open systems, is well-suited for cybersecurity where attacker–defender inter- actions are central. This paper bridges the gap between system security modelling and MAS verification, providing active defense orchestration with formal guarantees. Our contributions are (i) a general methodology for controlling active cyber defenses with formally verified specifications based on the attack–defense movement model (ADM), a new model of attacker and defender actions, (ii) an application of this methodology for adaptive honeypot control, which relies on a MAS logic contribution to express strategic properties such as attacker attribution, and (iii) VeriPot, a tool which implements the honeypot adaptation strategy extraction from the ADM.

ABSTRACT. Attack Trees (ATs) are widely used to model and analyze security risks. Quantitative AT analysis can furthermore express risk with multiple metrics such as required attacker cost, time, and skill. This gives a detailed security assessment of the system as a whole, but does not come with a notion of which attacks are most critical. Understanding such criticality can significantly contribute to risk prioritization. To fill these gaps in AT, we propose Importance Measures (IMs) for ATs that quantify how important a single attack step is to the overall success or likelihood of the attack. We analyze cost- and probability-based attack models that reflect common operational scenarios among researchers, such as persistent adversaries against systems with limited detection capabilities and single-attempt attacks in high-security environments. Our framework supports arbitrary monotone metrics and provides a framework allowing the study of many metrics. We apply our proposed framework to a real-world case study taken from the MITRE ATT&CK knowledge source. Our results show how importance measures can identify high-leverage attack steps that substantially reduce attacker effort or increase success probability, and how defenders can use our approach to prioritize mitigations under limited resources.

ABSTRACT. SMT solvers increasingly produce proof certificates to meet the trust requirements of safety-critical applications. However, eagerly justifying learned theory lemmas during solving constitutes a major performance bottleneck. Recent work mitigates this cost by emitting proof skeletons that record only SAT reasoning and unannotated theory lemmas, though existing approaches depend on new proof formats and specialized theory-specific tooling. We present a general approach that restricts SMT proof skeletons to core SMT reasoning: preprocessing, clausification, and unannotated theory lemmas. We develop external tools for SAT reasoning and proof trimming that reduce the number of theory lemmas requiring justification. An experimental evaluation using the SMT solver cvc5 on SMT-LIB benchmarks across the UF, LIA and LRA theories, with and without quantifiers, demonstrates faster solving and competitive checking performance compared to eager proof production, particularly on quantifier-free problems.

ABSTRACT. Eunoia is a logical framework designed for specifying the proofs and proof systems of SMT solvers, namely CVC5. We present a translation from a core fragment of Eunoia to the 𝜆Π-calculus modulo rewriting as implemented by the LambdaPi proof assistant. The translation is implemented by our tool eo2lp, which we use for generating LambdaPi encodings of (a) a large fragment of the Cooperating Proof Calculus (CPC), the Eunoia signature defining CVC5’s proof system, and (b) proofs produced by CVC5 on unsat problems from various fragments of SMT-LIB.

ABSTRACT. cvc5 is a state-of-the-art proof-producing SMT-solver, capable of solving formulas over a myriad of theories, including that of unicode strings. Matching regular expressions against candidate strings is done numerous times during the solving process of string constraints, and forms a bottleneck in proof-checking for unsatisfiable formulas. In this paper, we describe three approaches for checking regular expressions in proofs produced by cvc5. We also describe their implementation in the Eunoia proof-checking framework, and evaluate them on proofs produced by cvc5 for unsatisfiable SMT-LIB benchmarks for quantifier free logics containing strings.

ABSTRACT. SMT solvers are used in many safety critical applications. To provide evidence of the correctness of their answers some SMT solvers generate externally checkable proof certificates. We present a high performance checker for SMT proofs called Ethos. In contrast with other dedicated SMT proof checkers, Ethos does not implement a fixed proof calculus. Instead, it lets users provide their own proof calculi using the declarative language Eunoia which has been designed to make this easy and convenient by extending the familiar SMT-LIB syntax. We give a short overview of Eunoia and then focus on Ethos itself. We describe multiple optimization and implementation details that ensure that Ethos is fast and practical. We also evaluate Ethos on proofs generated by cvc5, showing that the flexibility of Ethos allows us to efficiently check fine-grained proofs, containing no proof holes, over all SMT-LIB logics without floating points.

ABSTRACT. Almost Fair Simulations were recently introduced as a technique for interactive proofs of language inclusion between Büchi automata. The presented deductive system enables cyclic proofs, but is incomplete for fair similarity, a standard notion of refinement for Büchi automata. In this paper, we address this shortcoming by presenting a new deductive system for language inclusion of Büchi automata that preserves the simplicity of Almost Fair Simulations, with the additional benefit of being complete for fair similarity. We mechanized the soundness and the completeness proofs of our new system in the Rocq proof assistant. The proofs rely on a new technique we call nested parameterized coinduction, an adaptation of Hur's et al. parameterized coinduction for the difficult case of proofs by coinduction-induction-coinduction.

ABSTRACT. Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. Although these criteria are well studied on paper and implemented in tools, a unified, machine-checked account that relates them to the (abstract) Infinite Descent property has been missing. We present an Isabelle/HOL mechanization of this landscape. We develop a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable Isabelle lemmas for $\omega$-regular reasoning over streams and for Büchi-automata constructions needed by the inclusion proofs.

ABSTRACT. Quantum compiler optimization relies on rewriting rules derived from equivalences between quantum circuits, yet prior work has identified thousands of such identities, creating substantial challenges for their storage, management, and effective application. For many widely used unitary gate sets, including Clifford+T, this apparent complexity is largely redundant, raising a fundamental question: How many quantum circuit identities are actually needed to generate all others? In this work, we provide strong evidence that a small set of independent identities suffices to generate all circuit equivalences of bounded depth. Surprisingly, for circuits on up to nine qubits in which each side of an equality has depth at most ten, fewer than twenty independent identities are sufficient to derive all others, and for circuits on up to five qubits with depth at most ten, only 17 rules--each involving at most three qubits--are enough. These results enable significantly more compact and efficient rewriting systems for quantum compiler optimization and reveal underlying algebraic structure in common gate sets, showing that the vast majority of known circuit identities are consequences of a small foundational basis.

ABSTRACT. Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when specifications are given directly as automata, prior frameworks incur exponential blow-up when translating high-level set-based assertions into automata, which severely limits practicality. We introduce an extended set-based specification language and a specification-to-automata translation algorithm whose complexity is linear in the number of qubits, enabled by controlled automaton construction and qubit reordering. The resulting compact automata enable fully automatic Hoare-style verification of fixed-qubit quantum programs at previously infeasible scales, while substantially improving expressiveness without compromising efficiency.

ABSTRACT. Ensuring ancilla safety is a critical correctness requirement for quantum compilation, since ancilla qubits are routinely introduced to implement complex operations with fewer gates and reduced depth. However, formally verifying this property is computationally hard due to state-space explosion in the number of qubits, particularly for dirty ancilla, which carry unknown initial states and must be restored after use. We propose an end-to-end verification-and-repair framework that rigorously addresses both clean and dirty ancilla safety. Our core contribution is a two-step reduction strategy: we first prove that verifying an m-qubit dirty ancilla register decomposes into 2m independent clean ancilla safety checks; subsequently, we reduce each clean ancilla safety instance to an algebraic commutativity check against Pauli-Z and Pauli-X operators. This approach yields an efficient and naturally parallel verifier and enables actionable diagnosis by classifying violations into logic errors and phase errors. Leveraging this diagnosis, we further design lightweight repair routines that append local single-qubit rotations to eliminate a broad class of local ancilla faults. We implement the full pipeline in a prototype tool using a dual-backend architecture combining decision diagrams and weighted model counting, and validate it on diverse circuits ranging from arithmetic benchmarks to Grover’s algorithm. Our experiments demonstrate scalability to thousands of qubits and show that the proposed repairs effectively improve ancilla safety while preserving circuit functionality.

ABSTRACT. Matrix product states (MPS) are the standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying spatial and size-dependent properties of physical many-body states, where the key parameter is the chain length. This paper takes a step toward bridging this gap. We propose Linear Chain Logic (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and long-range asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analyzed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given length and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.

ABSTRACT. We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal. Our approach encodes quantum states, operations, and measurements into \uppaal timed automata with data extensions and external C++ function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol---a time-slotted generalization of superdense coding---combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

ABSTRACT. We present Quokka, a versatile, open-source Python library for quantum-circuit analysis. Quokka reduces various simulation, verification, and synthesis tasks to (maximum) weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. Quokka provides multiple encodings by treating circuit semantics in different algebraic bases and enables key performance tradeoffs by supporting various equivalence checking methods. Moreover, it realizes approximate analysis, where approximation is quantified via circuit fidelity, which is crucial for synthesizing circuits in different gate sets and for real-world, noisy quantum computing, where circuit depth is limited, as approximations allow for large reductions in circuit complexity. This paper demonstrates the design, extensibility, and use of Quokka.

ABSTRACT. Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminates in the presence of length constraints. To do this, we introduce extended word equations, a mathematical model of a word equation with partial information about length constraints. We then define extended Nielsen transformations, which adapt Nielsen transformations to the setting of extended word equations. We provide a partial characterization of when repeatedly applying extended Nielsen transformations to an extended word equation is guaranteed to terminate.

ABSTRACT. We consider the closure of three of the most classical combination properties, namely, stable infiniteness, gentleness and shininess (or, equivalently for decidable theories, strong politeness), under intersection and maximal combinability. Starting with these three properties, we compute every possible intersection, and then compute the maximal sets of theories that can be combined with each resulting intersection. We iterate this process until no new classes are identified. How many properties will we end up with?

ABSTRACT. We present a sequent calculus for Scott's theory of classes founded on positive free logic. Cut elimination, generalised subformula property and consistency are shown to hold, also in the intuitionistic variant. Eventually the calculus is extended to cover the original Zermelo's set theory Z without the axiom of choice by means of (systems of) rules. The calculus for Z preserves cut elimination, moreover, some of its subsystems and extensions are also provably consistent.

ABSTRACT. Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

ABSTRACT. The two-watched literal scheme, a core component of efficient CDCL (Conflict-Driven Clause Learning) implementations for propositional logic, is extended to first-order logic. Given a set of first-order clauses and a set of ground literals, our lifted two-watched literal scheme efficiently detects all propagating and false clauses with respect to the ground literals. We present the algorithm as a system of rules and prove its soundness and completeness. Additionally, we provide an implementation of the two-watched scheme, which outperforms a standard dynamic programming approach for detecting propagatable literals and conflicts, especially when dealing with long clauses.

ABSTRACT. Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous systems (SRA) is challenging due to process-process and process-scheduler interactions. In this paper, we tackle the problem of verifying configurable SRA. A configurable SRA describes an unbounded family of possible SRA, each resulting from an instantiation satisfying given configuration constraints; our goal is proving at once that every legal instantiation of a configurable SRA is correct. We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations. The approach is grounded in (object-oriented) first order logic, requires reasoning over quantified statements, and leverages the Dafny software verifier as a backend. An experimental evaluation on industrial case studies demonstrates that the framework scales effectively and enables practical reasoning about complex parameterized behaviors.

ABSTRACT. The theory of simplicial complexes is a cornerstone of topology, offering a sophisticated tool for computing invariants. We present a formalization of abstract simplicial complexes and stellar subdivisions in the Lean proof assistant. We adopt a purely combinatorial framework in order to provide a cohesive foundation for studying the theory of stellar subdivisions as seen in many contexts of combinatorial topology. In particular, we provide formalizations of morphisms between abstract simplicial complexes; several crucial constructions and operations on complexes, such as links and joins; and perform a comprehensive study of how stellar subdivisions interact with these operations. We state and prove a number of identities commonly used in the study of triangulated manifolds, such as deriving equivalences between links in an abstract simplicial complex $K$ and in a stellar subdivision $\sigma_s K$, including results with no references in the standard literature. To our knowledge, this is the first formalization of stellar subdivisions in any proof assistant.

ABSTRACT. We present an Isabelle/HOL formalisation of the foundations of analytic number theory related to modular forms. We begin by refactoring and extending the existing library on elliptic functions, adding the theorem that every elliptic function can be written in terms of the Weierstraß elliptic function ℘ and the addition theorem for ℘, which links complex lattices to elliptic curves. Next, we develop an extensive library on Jacobi theta functions, including well-known results such as the Jacobi triple product, the Pentagonal Number Theorem, and the Rogers–Ramanujan identities. Finally, we apply this library to the study of the Dedekind η function and the ‘forbidden’ Eisenstein series G2. In all of this, we aim for short and clean proofs, building a library of reusable lemmas.

ABSTRACT. In 1930, Keller conjectured that every gap-free tiling of R^n by n-dimensional unit cubes must contain cubes that fully share an (n − 1)-dimensional face. Keller’s conjecture holds for n ≤ 7 and fails for n ≥ 8. The final case, n = 7, was settled in 2020 using a mix of traditional and automated reasoning. The result was obtained by reducing the conjecture to a set of clique-existence problems, encoding those problems into propositional logic, breaking symmetries, and solving them with a SAT solver. In this paper, we present an end-to-end verification in Lean 4 of Keller’s conjecture for all dimensions. First, we simplify a prior reduction of Keller’s conjecture to the clique-existence problems. We then verify an improved SAT encoding of those problems and some associated symmetry reasoning. Throughout our work, we sought to maximize the synergy between interactive and automated techniques while minimizing human proof burden. In particular, the symmetry reasoning was split between Lean and a clausal proof system, since neither was suitable on their own for verifying all the symmetry reasoning. We discuss how and why we chose to split the reasoning across these systems, based on their relative strengths and weaknesses.

ABSTRACT. A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the AnyMiss(2, 300) weakly-hard constraint stipulates that in every window of 300 consecutive jobs, at most 2 deadlines are missed. The weakly-hard model is the state-of-the-art for industrial dependability-by-design of control systems that tolerate deterministic failures. Weakly-hard constraints correspond to regular languages. The size of the minimal finite state machine that recognizes whether a string satisfies the constraint (about 45k states for AnyMiss(2, 300)) is a notorious impediment for the verification of control system properties. This paper discusses an over-approximation of the language that allows us to provide sound safety guarantees for control systems under deadline misses that would be out of reach using the minimal finite state machine. We present a compressed language acceptor and prove that it simulates the original finite state machine. We study language cardinality properties, and report on empirical results that show how the new acceptor can be embedded in the control design workflow, leading to verifying safety for systems for which the state-of-the-art tools do not provide answers.

ABSTRACT. The reliability of autonomous systems depends on their robustness, i.e., their ability to meet their objectives under uncertainty. In this paper, we study spatiotemporal robustness of temporal logic specifications evaluated over discrete-time signals. Existing work has proposed robust semantics that capture not only Boolean satisfiability, but also the geometric distance from unsatisfiability, corresponding to admissible spatial perturbations of a given signal. In contrast, we propose spatiotemporal robustness (STR), which captures admissible spatial and temporal perturbations jointly. This notion is particularly informative for interacting systems, such as multi-agent robotics, smart cities, and air traffic control. We define STR as a multi-objective reasoning problem, formalized via a partial order over spatial and temporal perturbations. This perspective has two key advantages: (1) STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations, and (2) STR can be computed using tools from multi-objective optimization. To navigate computational challenges, we propose robust semantics for STR that are sound in the sense of suitably under-approximating STR while being computationally tractable. Finally, we present monitoring algorithms for STR using these robust semantics. To the best of our knowledge, this is the first work to deal with robustness across multiple dimensions via multi-objective reasoning.

ABSTRACT. We consider the problem of controlling a multi-mode system w.r.t. a safety goal in the Filippov sliding-mode semantics. When the goal can be enforced, we present a symbolic algorithm that enhances the previously known solution. When the goal cannot be enforced, we compare different natural best-effort criteria, identify the most promising one, and design a symbolic algorithm that synthesizes the corresponding myopically optimal control policy. We prove that the synthesized policy enjoys a regularity property known as a tame topology.

ABSTRACT. Agents in cyber-physical systems are increasingly entrusted with safety-critical tasks. Ensuring safety of these agents often requires localizing the pose for subsequent actions. Pose estimates can, e.g., be obtained from various combinations of lidar sensors, cameras, and external services such as GPS. Crucially, in safety-critical domains, a rough estimate is insufficient to formally determine safety, i.e., guaranteeing safety even in the worst-case scenario, and external services might additionally not be trustworthy. We address this problem by presenting a certified pose estimation in 3D solely from a camera image and a well-known target geometry. This is realized by formally bounding the pose, which is computed by leveraging recent results from reachability analysis and formal neural network verification. Our experiments demonstrate that our approach efficiently and accurately localizes agents in both synthetic and real-world experiments.

ABSTRACT. We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches to this problem rely on encoding the state-transition matrix using either explicit or symbolic representations. While more recent work frames the verification problem as probabilistic inference, this approach does not appear to improve scalability across the board. Our insight is to cast probabilistic model checking of Markov chains as computations over tensors. This methodology enables the use of off-the-shelf compiler toolchains for optimized execution of these tensor computations on hardware accelerators. We prove the soundness of the methodology of mapping probabilistic model checking to tensor computations. We implement our approach in a tool called Tessa. Empirical evaluation shows that Tessa easily unlocks massive speedups over state-of-the-art methods on benchmarks from the literature.

ABSTRACT. Computing optimal conditional reachability probabilities in Markov decision processes (MDPs) is tractable by a reduction to reachability probabilities. Yet, this reduction yields cycling, challenging MDPs that are often notoriously hard to solve. We present an alternative, practically efficient method to compute optimal conditional reachabilities. The new method is numerically stable, can decide the threshold problem in linear time on acyclic MDPs, and yields performance comparable to standard reachability queries. We also integrate the method in an abstraction-refinement framework to analyse millions of Markov chains at once. We demonstrate the efficacy of the new methods on benchmarks from Bayesian network analysis, probabilistic programs, and runtime monitoring and show speed-ups up to multiple orders of magnitude.

ABSTRACT. Machine Learning (ML) inference is shifting from using pre-developed static, CUDA C++, GPU kernel libraries to using MLIR-based graph compilers that perform advanced optimizations and generate custom kernels. This paradigm shift reimagines how we achieve ML inference in safety-critical domains such as automotive applications. Traditional approaches relied on qualifying static kernel libraries—pre-built for fixed input shapes and parameter ranges—according to the ISO 26262 standard. However, the demanding performance requirements of diverse ML models and rapidly evolving hardware accelerators necessitate generating optimized kernels on the fly, which only ML graph compilers can provide. This paper presents an industrial experience report on a comprehensive verification framework for ML inference in automotive applications. We describe the transition from static kernels to dynamic ML graph compilation and introduce two complementary verification strategies: (1) formal methods targeting memory safety and concurrency properties in CUDA kernels and MLIR-based compiler; and (2) AI-driven testing for functional correctness. Our experience over multiple years of production use demonstrates that validating ML graph compiler output can achieve safety assurance levels comparable to compiler qualification while enabling performance and flexibility benefits. We discuss remaining challenges including scalability of formal verification and adapting to evolving compilers and hardware platforms.

ABSTRACT. \emph{Caesar} is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative \emph{intermediate verification language} based on the real-valued logic HeyLo. HeyVL allows to express a probabilistic program, its specifications, and proof rules in a programming-language-style, so that new proof rules can be easily integrated into the verifier. Caesar translates HeyVL programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes another backend based on probabilistic model checking for a subset of HeyVL. We report on the results of five years of development of Caesar, highlighting its main features and architecture. In particular, we highlight recent improvements such as additional proof rules, a model checking backend, and better diagnostics.

ABSTRACT. We present a tool for the compositional verification and correct-by-construction synthesis of stochastic world models---heterogeneous networks of interdependent stochastic models including discrete and continuous-time Markov chains, Markov decision processes (MDPs), partially observable MDPs, and stochastic multi-player games. Through its unique integration of multiple probabilistic and parametric model checking paradigms, our tool unifies the modelling, verification and synthesis of systems characterised by a combination of probabilistic and nondeterministic uncertainty, discrete and continuous-time behaviour, partial observability, and multi-agent interaction.

ABSTRACT. We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the 𝜋-calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm. We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.

ABSTRACT. Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework.

ABSTRACT. HyperLTL extends Linear Temporal Logic (LTL) by introducing trace variables that range over a domain of traces, and quantification over traces, making it possible to relate the assignments of propositional variables along multiple traces. This leads to HyperLTL becoming a predominant specification logic for hyperproperties, which are properties of sets of traces as opposed to individual traces. Satisfiability of HyperLTL is not recursively enumerable. Hence algorithmic methods cannot take the role of deduction for establishing validity. Furthermore, quantification over traces is restricted to be outside the scope of temporal operators in HyperLTL. In this paper, we consider HyperLTL∗, which is the generalization of HyperLTL by dropping this restriction. We pro- pose a proof system for HyperLTL∗, where completeness is achieved by allowing an ω-rule. Weaker finitary rules such as what can be useful for interactive theorem proving can be derived using the ω-rule. We give examples of the use of the proof system on complicated HyperLTL for- mulas which would be hard to derive automatically. We also discuss the expressiveness of HyperLTL∗ and the potential for using first-order logic theorem provers based on it. theorem provers based on it.

ABSTRACT. Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. Most algorithms for deciding if a given system satisfy a given hyperproperty rely on a user-specified abstraction of the system. In this paper, we suggest a novel automatic abstraction-refinement algorithm for hyperproperties verification. Our approach is based on predicate abstraction and the recently introduced reduction of hyperproperties verification to satisfiability of Constrained Horn Clauses (CHCs). Moreover, it formalizes and uses CHC-based refinement for counterexamples in the shape of a directed acyclic graph. We implemented our new algorithm on top of the SMT solver Z3. Our experimental evaluation shows our automatic abstraction refinement algorithm can solve a variaty of hyperproperty verification problems, completely automatically. This is in contrast to other existing techniques that require a user-given abstraction.

ABSTRACT. Uniform interpolation is a strong form of interpolation providing an interpretation of propositional quantifiers within a propositional logic. Pitts’ seminal work establishes this property for intuitionistic propositional logic relying on a sequent calculus in which naïve backward proof-search terminates. This constructive approach has been adapted to a wide range of logics, including intuitionistic modal logics. Surprisingly, no intuitionistic modal logic with independent box and diamond has yet been shown to satisfy uniform interpolation. We fill in this gap by proving the uniform interpolation property for Constructive K (CK) and Wijesekera's K (WK). We build on Pitts' technique by exploiting existing terminating calculi for CK and WK, which we prove to eliminate cut, and formalise all our results in the proof assistant Rocq. Together, our results constitute the first positive uniform interpolation results for intuitionistic modal logics with diamond.

ABSTRACT. We study the problem of synthesizing programs from non-linear real arithmetic (NRA) specifications. Existing techniques, such as syntax-guided synthesis (SyGuS), fail to synthesize programs when the specification is unrealizable. We argue this is unsatisfactory in many situations, and aim to synthesize programs from arbitrary NRA specifications, such that for any input, the synthesized program either produces outputs satisfying the specification or correctly reports non-existence of any such output. To avoid rounding errors inherent in floating-point arithmetic, we restrict our programs to operate on rational inputs and outputs, thereby strictly generalizing beyond programs that work with floating-point numbers. We first show that our variant of the synthesis problem is as hard as a long-standing open problem in number theory, and that synthesizing loop-free programs from arbitrary NRA specifications with rational inputs and outputs is impossible in general. Second, we present a sound and complete synthesis algorithm for the case where the specification involves a single output variable. We also show that for realizable specifications, a program generated by SyGuS for NRA (treating inputs and outputs as reals) serves as a solution to our problem, where inputs and outputs are rationals. Third, we provide a sound (but necessarily incomplete) synthesis algorithm for the general case of specifications in NRA. We have implemented our approach in a prototype tool that solves many benchmarks beyond the reach of state-of-the-art SyGuS tools, even when we render the specification realizable.

ABSTRACT. Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the communication pattern of the session is described using a global type. Then the global type is projected on to a local type for each participant, and the individual processes making up the session are type-checked against these projections. Typed sessions possess certain desirable properties such as safety, deadlock-freedom and liveness. In this work, we present the first mechanised proof of liveness for synchronous multiparty session types in the Rocq Proof Assistant. Building on recent work, we represent global and local types as coinductive trees using the paco library. We use a coinductively defined subtyping relation on local types together with another coinductively defined plain-merge projection relation relating local and global types. We then associate collections of local types, or local type contexts, with global types using this projection and subtyping relations, and prove an operational correspondence between a local type context and its associated global type. We utilise this association relation to prove the safety and liveness of associated local type contexts and, consequently, the multiparty sessions typed by these contexts. Besides clarifying the often informal proofs found in the MPST literature, our Rocq mechanisation also enables the certification of liveness properties of communication protocols. Our contribution amounts to around 14K lines of Rocq code, available at https://github.com/omerskeskin/mpstlive .

ABSTRACT. In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style scripts to declarative Isar. This allows users to write complex, possibly fragile apply-style scripts, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.

ABSTRACT. We present a Rocq library for monoidal categories, which includes a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if they were strict, inferring MacLane isomorphims automatically in the background. Together with an external tool for visualising and editing string diagrams, this make it possible to perform rewriting steps in monoidal categories graphically, and to translate them back into formal proofs which are concise and readable.