ABSTRACT. Lean is an open-source theorem prover and dependently-typed programming language that has seen rapid adoption across mathematics, software verification, and AI research. Its Mathlib library is among the largest formalized mathematical developments in existence. Lean's design emphasizes extensibility: the system is implemented in Lean itself, and a powerful meta-programming framework enables users to build custom automation and domain-specific tools. This talk traces Lean's history from its origins in 2013 through four major rewrites to the present day, discusses the design decisions that shaped the system and the lessons learned along the way, and concludes with current priorities at the Lean Focused Research Organization.

ABSTRACT. The verification of \emph{reductions}, representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syntactic reductions, which we call \emph{natural reductions}. Natural reductions are specified by introducing atomic blocks and global rendezvous points in the parameterized program's thread template. We study the problem of deciding whether a given natural reduction is sound wrt.\ a given (semi-)commutativity relation. In the case that there is no synchronization between threads, we present a sound and complete polynomial-time algorithm. In the case where synchronization is considered, we provide a general lower bound for the problem (parametric in the synchronization mechanism), and show that the problem is coNP-hard already for a simple mechanism like locking.

ABSTRACT. Mutexes are fundamental synchronization primitives in concurrent programming, but their improper use can lead to deadlocks. Conventional assume-based modeling abstracts mutex semantics via assumptions, simplifying safety verification but hindering deadlock verification. Although prior efforts have aimed to address this limitation, we show that state-of-the-art methods remain inaccurate. In this paper, we propose a novel modeling approach that captures mutex semantics using ordering constraints, enabling accurate deadlock verification within partial-order-based verification frameworks. We formally prove the correctness of our method and implement it in a prototype tool, DEAGLE-DL. We evaluate DEAGLE-DL against a state-of-the-art bounded model checker ESBMC that employs the conventional modeling approach, and a state-of-the-art static analysis tool for deadlock detection. Our experiments show that DEAGLE-DL significantly outperforms both tools in terms of precision, while maintaining substantial efficiency.

ABSTRACT. This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness for them in the form of a universally quantified inductive invariant, where the quantification is over the nodes in the topology. We illustrate that under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme in which the verification of the parameterized family is reduced to a set of local proofs, in a complete manner. We propose a verification algorithm, which is implemented as a tool, and demonstrate through a set of benchmarks over several different topologies that our approach is effective in proving parameterized programs safe.

ABSTRACT. This paper introduces several techniques that improve the scalability of the deductive verification of data-level programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct in a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the \vercors program verifier. We illustrate how our techniques improve scalability on a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted the verification of results which were previously unobtainable and significantly reduced the verification time.

ABSTRACT. Remote Direct Memory Access (RDMA) is a technology that allows direct memory access from the memory of one computer into that of another without involving either one’s operating system. This enables high-throughput, low-latency networking, which is especially useful in massively parallel computer clusters. In this paper, we study the reachability and robustness problems for RDMA programs. We show that reachability is undecidable in general, even for a restricted fragment of the model. We then focus on robustness, which asks whether a program exhibits the same behaviours under the RDMA and sequential consistency (SC) semantics, and prove that this problem is decidable. Our central technical result establishes a normal form for robustness violations, showing that any non-robust program admits a violating execution of a specific form. We then leverage this normal form to obtain a decision procedure that reduces robustness to reachability in finite-state programs with counters, yielding an EXPSPACE upper bound in the general case, and a PSPACE upper bound in the absence of poll operations. Finally, we also show that both of these bounds are optimal.

ABSTRACT. Operating a network is a daunting task. Operating one at a global scale, with stringent service objectives and requirements to be available during maintenance and failures, is even more so. At Google, we operate such a network. This paper details our experience applying formal methods to some of the networking protocols that are developed and maintained by in-house engineers. These protocols centrally route network traffic to respond to changes in demand, react to network failures, and allow for maintenance and upgrades. We used formal methods to target a class of bugs stemming from unclear specifications, unintended system interactions, and logical errors at the specification level. We show how we modeled our protocols using an off-the-shelf model checker and a custom harness to scale the model horizontally. We were able to recreate several recent bugs and verify that the fixes implemented were correct. Finally, we present a method called state projection that we used to increase confidence in the coverage of our models, which we added to the TLC model checker for TLA+. We created 7 different TLA+ models and showed that they were effective at recreating bugs and verifying our fixes to those bugs.

ABSTRACT. 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.

ABSTRACT. In recent years, protocol state fuzzing has emerged as an effective technique to analyze and test network protocol implementations, uncovering numerous security vulnerabilities, bugs, and non-conformance issues in them. This tool paper presents ProtocolState-Fuzzer (PSF for short), an open source, generic, modular, and extensible framework for state machine learning and testing of network protocol implementations. We describe the distinctive features and support that PSF offers, its system architecture, and briefly overview the protocol-specific state fuzzers that currently use PSF as their basis.

ABSTRACT. We present Kofola, an efficient tool for complementing and inclusion checking over Büchi automata. Complementation and inclusion checking for Büchi automata are the cornerstones of many verification problems such as model checking, monitoring, and theorem proving. Kofola implements the state-of-the-art modular complementation framework that partitions the input Büchi automata to apply, for each strongly connected component, the complementation algorithm leveraging the most its structural properties. Inspired by the modular complementation, Kofola also supports modular inclusion checking along with new heuristics. Notably, to allow termination as soon as possible, we have developed a new on-the-fly emptiness checking algorithm for the simple generalized Rabin pair condition, which is the acceptance condition used by our complementation. Empirical evaluation shows that Kofola is highly competitive against the state-of-the-art complementation and inclusion checking tools, being the most robust of the tools that we evaluated and outrunning them often by several orders of magnitude on many benchmarks obtained from practical applications.

ABSTRACT. P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus, a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence. Octopus produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample packet witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes on consumer hardware. We report on the tool’s implementation and evaluate its usability in networking contexts.

ABSTRACT. Differential privacy (DP) is one of the most efficient tools for protecting the privacy of individual data holders under computation. This property guarantees that the computation outputs for every pair of adjacent input sets are statistically indistinguishable with respect to a given parameter ε, which is independent of the likelihood that specific inputs occur or not. While the distribution of input sets is generally unknown, in some use cases (approximate) information about it might be available. If the latter is the case, two adjacent inputs of one individual are sometimes already obfuscated by other inputs and the computation itself (i.e., without any additional noise). For example, if the sum of n independent and identically distributed uniformly random bits outputs approximately n/2, both values for the first bit remain (almost) equally likely for large n. Based on this observation, we present a new DP mechanism that uses an estimate of the input distribution to reduce the noise addition (compared to standard DP) and hence improves the accuracy of the output. We first explore this idea in the central model, where a single central party collects all data. Then, we provide a new technique (possibly of independent interest) that allows multiple entities to jointly generate reduced noise, using the property of infinite divisibility. This allows each party to individually add noise to their respective inputs, e.g., in Federated Analytics applications. We apply our theoretical results, both for the single and multi-party setups, to perform data analysis over human resources data from different subsidiaries within a corporate group. Our benchmarks show that our new DP mechanism provides more accurate outputs while retaining the same privacy level as state-of-the-art DP approaches using the geometric mechanism.

ABSTRACT. As the use of differential privacy (DP) becomes widespread, the development of effective tools for reasoning about the privacy guarantee becomes increasingly critical. In pursuit of this goal, we demonstrate novel relationships between DP and measures of statistical disclosure risk. We suggest how experts and non-experts can use these results to explain the DP guarantee, interpret DP composition theorems, select and justify privacy parameters, and identify worst-case adversary prior probabilities.

ABSTRACT. The shuffle model, which anonymizes data by randomly permuting user messages, has been widely adopted in both cryptography and differential privacy. In this work, we present the first systematic study of the Bayesian advantage in re-identifying a user's message under the shuffle model. We begin with a basic setting: one sample is drawn from a distribution $P$, and $n - 1$ samples are drawn from a distribution $Q$, after which all $n$ samples are randomly shuffled. We define $\beta_n(P, Q)$ as the success probability of a Bayes-optimal adversary in identifying the sample from $P$, and define the additive and multiplicative Bayesian advantages as $\mathsf{Adv}_n^{+}(P, Q) = \beta_n(P,Q) - \frac{1}{n}$ and $\mathsf{Adv}_n^{\times}(P, Q) = n \cdot \beta_n(P,Q)$, respectively. We derive exact analytical expressions and asymptotic characterizations of $\beta_n(P, Q)$, along with evaluations in several representative scenarios. Furthermore, we establish (nearly) tight mutual bounds between the additive Bayesian advantage and the total variation distance. Finally, we extend our analysis beyond the basic setting and present, for the first time, an upper bound on the success probability of Bayesian attacks in shuffle differential privacy. Specifically, when the outputs of $n$ users—each processed through an $\varepsilon$-differentially private local randomizer—are shuffled, the probability that an attacker successfully re-identifies any target user's message is at most $e^{\varepsilon}/n$.

ABSTRACT. Pointwise maximal leakage (PML) is a per-outcome privacy measure based on threat models from quantitative information flow. Privacy guarantees with PML rely on knowledge about the distribution that generated the private data. In this work, we propose a framework for PML privacy assessment and mechanism design with empirical estimates of this data-generating distribution. By extending the PML framework to consider sets of data-generating distributions, we arrive at bounds on the worst-case leakage within a given set. We use these bounds alongside large-deviation bounds from the literature to provide a method for obtaining distribution-independent $(\varepsilon,\delta)$-PML guarantees when the data-generating distribution is estimated from available data samples. We provide an optimal binary mechanism, and show that mechanism design with this type of uncertainty about the data-generating distribution reduces to a linearly constrained convex program. Further, we show that optimal mechanisms designed for a distribution estimate can be used. Finally, we apply these tools to leakage assessment of the Laplace mechanism and the Gaussian mechanism for binary private data, and numerically show that the presented approach to mechanism design can yield significant utility increase compared to local differential privacy, while retaining similar privacy guarantees.

ABSTRACT. With the widespread adoption of graph-structured data, protecting the complex relational information between nodes and edges while preventing sensitive information leakage has become a critical challenge. However, existing edge protection methods either introduce noise directly into the adjacency matrix, resulting in significant information loss, or uniformly apply noise across all edges, leading to imbalanced privacy budget allocation and inefficiency. To address these issues, we propose DPEI, a Differential Privacy-based Edge Information protection solution designed to safeguard the edge relationships between two nodes, thus reducing the risk of privacy leakage and preventing attackers from repeatedly inferring internal community relationships from the released graph data. Specifically, DPEI achieves protection through PPO (Proximal Policy Optimization) based selection of locally optimal thresholds combined with adaptive Laplace noise operations, and attachment nodes below the threshold into high-information edges to enhance relational information protection. Subsequently, unlike traditional uniform allocation, DPEI distributes the privacy budget in proportion to the information content of each edge, ensuring that edges with higher information content receive stronger privacy protection. Extensive experiments conducted on three real-world graph datasets demonstrate that DPEI significantly outperforms existing methods across seven commonly used graph metrics, thereby validating its effectiveness and practicality.

ABSTRACT. We present a formalization of bounded operators on complex vector spaces in Isabelle/HOL. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces, Hilbert spaces) that complements and goes beyond the developments of real vectors spaces in the Isabelle/HOL standard library. We define the type of bounded operators between complex vector spaces (cblinfun) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the Jordan_Normal_Form AFP entry.

ABSTRACT. Understanding and certifying the generalization performance of machine learning algorithms---i.e.\ obtaining \emph{theoretical} estimates of the test error from a finite training sample---is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, \emph{Rademacher complexity} yields sharp, data-dependent bounds that apply well beyond classical $0$--$1$ classification. In this study, we formalize the generalization error bound by \emph{Rademacher complexity} in Lean~4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from \emph{countable} hypothesis classes (where measurability of suprema is straightforward in Mathlib) to \emph{separable} topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under $\ell_2$ and $\ell_1$ regularization, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.

ABSTRACT. This paper presents \emph{differential-algebraic logic} (\dAL), an axiomatic framework for the deductive verification of \emph{differential-algebraic programs} (DAPs), which extend hybrid dynamical systems with differential-algebraic equations (DAEs). In particular, this paper develops a refinement calculus that allows for the sound comparison between trajectories of differential-algebraic equations, crucially utilizing a novel trace-based semantics. Such a refinement calculus then allows for the incremental verification/simplification of complicated DAEs, while ensuring correctness at each step by the soundness of the axiomatization. In addition, this paper presents an application of the axiomatization by establishing its completeness in certifying index reductions of DAEs, providing trustworthy syntactic proofs of correctness at each step of the reduction.

ABSTRACT. Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need of repeatedly rechecking their safety in full after every change. We present a method for proving that system refactorings preserve their required properties by transferring the proof along the modification. It is based on differential refinement logic (dRL), with which one can simultaneously and rigorously refer to properties of the systems and the relation between a refactored system with its original version. Refinements represent a uniform way of expressing different types of hybrid system refactorings, including those that introduce auxiliary variables. Furthermore, we show how these refactorings can be proved automatically, and/or reduce to a modular proof solely about the local change rather than about the whole system.

ABSTRACT. This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. By small, natural, and practically meaningful syntactic restrictions, specifications are ensured (by construction) to be topologically open and, thus, robust with respect to infinitesimal perturbations without explicit quantitative margins of error in the syntax or in proofs. The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. The proof is constructive, self-contained, and demonstrates how robustly-correct hybrid systems reachability specifications can be automatically verified through proof.

ABSTRACT. We study concurrent graph games where $n$ players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other. We show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals ($\exists\mathbb{R}$) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is $\NP$-hard. For the almost-sure reachability problem, we prove $\NP$-completeness. We introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop.

ABSTRACT. We study the problem of generating paths on a graph that satisfy a collection of $\omega$-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 $\omega$-regular objectives. In particular, B\"uchi objectives admit universal composition of finite-memory policies without scheduler communication; co-B\"uchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.

ABSTRACT. We present a new Programming-by-Examples (PBE) approach to repairing regex-dependent string-manipulation programs. Our approach has the following key features: (1) the support for a {\em wide range of functions} including regex-dependent functions such as {\tt replaceAll}, {\tt match}, {\tt split}, list manipulation functions such as {\tt map}, {\tt reduce}, {\tt filter}, and numerical functions such as {\tt max}, {\tt min}, {\tt pow}, (2) the support for {\em real-world regexes} with non-standard semantics such as greedy/lazy Kleene star and extensions such as lookarounds and backreferences, (3) the focus on a {\em method-chaining style} that starts the chain of calls with a regex-dependent function, reflecting a code style used in the real-world, and (4) novel {\em origin-enriched} examples that allow users to communicate {\em intensional} behavior of programs in addition to the standard extension behavior communicated via ordinary input-output examples, and a novel {\em origin-tracking} semantics that formally defines when a program conforms to the behavior stipulated by such examples. We have implemented our approach as a tool named R3-S3 and evaluated it on real-world benchmarks collected from GitHub and StackOverflow. The results show that R3-S3 finds high-quality repairs efficiently.

ABSTRACT. Component-based synthesis (CBS) aims to generate loop- free programs from a set of libraries whose methods are annotated with specifications and whose output must satisfy a set of logical constraints, expressed as a query. The effectiveness of a CBS algorithm critically de- pends on the severity of the constraints imposed by the query. The more exact these constraints are, the sparser the space of feasible solutions. This maxim also applies when we enrich the expressivity of the specifi- cations affixed to library methods. In both cases, the search must now contend with constraints that may only hold over a small number of the possible execution paths that can be enumerated by a CBS procedure. In this paper, we address this challenge by equipping CBS search with the ability to reason about logical similarities among the paths it explores. Our setting considers library methods equipped with refinement-type specifications that enrich ordinary base types with a set of rich logical qualifiers to constrain the set of values accepted by that type. For efficient representation and enumeration of this space, we introduce a novel tree automata variant called Liquid Tree Automata (LTA) whose construction is driven by the typing rules of a refinement type system. This allows us to leverage subtyping constraints over the refinement types associated with enumerated terms to enable reasoning about similarity among candidate solutions as search proceeds, using this notion of simi- larity to eagerly merge LTA states. By doing so, we avoid exploration of semantically similar paths, leading to a significantly improved search pro- cedure. We present an implementation of this idea in a tool called Hegel and provide a comprehensive evaluation that demonstrates Hegel’s abil- ity to synthesize solutions to complex CBS queries that go well-beyond the capabilities of the existing state-of-the-art.

ABSTRACT. Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guid- ance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.

ABSTRACT. Syntactic obligations is 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 huge runtime improvements in translation and synthesis.

ABSTRACT. Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present sweap, a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. sweap implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. sweap supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the Issy tool, and our own bespoke input. We present a mature version of sweap with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that sweap outperforms its only competitor in this domain.

ABSTRACT. Quantitative information flow (QIF) is concerned with assessing the leakage of information in computational systems. In QIF, there are two main perspectives for the quantification of leakage. On one hand, the static perspective considers all possible runs of the system in the computation of information flow, and is usually employed when preemptively deciding whether or not to run the system. On the other hand, the dynamic perspective considers only a specific, concrete run of the system that has been realised, while ignoring all other runs. The dynamic perspective is relevant for, e.g., system monitors and trackers, especially when deciding whether to continue or to abort a particular run based on how much leakage has occurred up to a certain point. Although the static perspective of leakage is well-developed in the literature, the dynamic perspective still lacks the same level of theoretical maturity. In this paper, we take steps towards bridging this gap with the following key contributions: (i) we provide a novel definition of dynamic leakage that decouples the adversary’s belief about the secret value from a baseline distribution on secrets against which the success of the attack is measured; (ii) we demonstrate that our formalisation satisfies relevant information-theoretic axioms, including non-interference and relaxed versions of monotonicity and the data-processing inequality (DPI); (iii) we identify under what kind of analysis strong versions of the axioms of monotonicity and the DPI might not hold, and explain the implications of this (perhaps counter-intuitive) outcome; (iv) we show that our definition of dynamic leakage is compatible with the well-established static perspective; and (v) we exemplify the use of our definition on the formalisation of attacks against privacy-preserving data releases.

ABSTRACT. We study privacy guarantees in the framework of pointwise maximal leakage (PML) that satisfy two requirements: they are robust under post-processing and upper bound the failure probability, i.e., the probability that the information leakage exceeds a given threshold. We first examine two candidate definitions inspired by (approximate) differential privacy and show that neither one satisfies both requirements simultaneously. We then introduce the notion of the PML envelope, which quantifies the largest amount of information leakage about a secret after arbitrary post-processing of a mechanism’s output. By construction, the PML envelope satisfies both requirements. We discuss basic structural properties of the envelope, such as monotonicity, and derive general upper and lower bounds. We further analyze the envelope for two widely used privacy mechanisms: the PML-extremal mechanisms in the high-privacy regime and randomized response. Overall, this work establishes the PML envelope as a natural and operationally meaningful definition for providing privacy guarantees that are preserved under arbitrary downstream transformations.

ABSTRACT. Local Differential Privacy (LDP) has become the de facto standard for privacy-preserving data collection in large-scale systems, in particular for the purpose of estimating frequencies. However, the current research landscape lacks a systematic and principled way to compare LDP protocols. The parameter ε of LDP is considered the measure of privacy, but it only bounds worst-case distinguishability. Other comparisons rely on utility-driven analyses, where mechanisms are ranked based on their ability to preserve data utility for a given privacy budget ε. Both such kinds of comparisons fail to account for the strength of protocols against diverse attacker models. In this paper, we propose a framework for analyzing LDP frequency estimation protocols through the lens of Quantitative Information Flow (QIF). By modeling LDP mechanisms as probabilistic channels, we leverage the concept of refinement (Blackwell ordering) to establish more principled classifications. This approach allows us to determine when one protocol is intrinsically superior to another for all possible adversaries, and to discuss the implications for utility. In particular, our analysis uncovers cases where protocols previously deemed "optimal" are, in fact, incomparable with, or strictly dominated by, other protocols. We provide a formal QIF-based treatment of seven state-of-the-art protocols, including Generalized Randomized Response (GRR), local hashing variants (BLH, OLH), unary encoding schemes (SUE, OUE), and Thresholding with Histogram Encoding (THE). This perspective bridges the gap between the LDP and formal methods communities and enables principled, adversary-aware reasoning about locally private systems.

ABSTRACT. Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, a useful operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.

ABSTRACT. This article describes the first mechanized proof of functional correctness of an algorithm due to Pornin (2020), for computing modular inverses via an optimized extended binary GCD algorithm. This algorithm is widely used in cryptography applications, due to its speed and constant-timeness. But this speed comes from the use of approximate computations during its loop iterations. In particular, the pen-and-paper proof of the fact that sufficiently many loop iterations were performed is especially intricate (and the originally published version was actually wrong), which negatively impacts the trust in the applications that rely on the algorithm. In this work, we expand the notes provided in the original description by Pornin into a complete formal proof. We discuss the challenges raised by its mechanization, which eventually relies on the collaboration of deductive program verification and interactive theorem proving through the use of the tools Rocq and Why3.

ABSTRACT. The Garsia–Wachs algorithm is an algorithm for finding a leaf-labeled binary tree whose leaf sequence exactly matches the input weight sequence and whose cost is as small as possible, where the cost is the sum of the weights labeling the leaves multiplied by their levels. The algorithm, along with a proof of correctness due to Kingston, is presented in Knuth's The Art of Computer Programming, Vol. 3. The algorithm comes in two versions, the naive and the optimized. Both versions have quadratic time complexity, but the optimized version can be fine-tuned with a suitable data structure to yield an O(n log n)-time algorithm. I implement and verify a variant of each version of the algorithm in the verification-aware programming language Dafny. Unlike all previous presentations of the algorithm, these variants construct the desired optimum tree directly, without detour through a "nonalphabetic" tree whose leaf sequence is a rearrangement of the input sequence.

ABSTRACT. We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable for automated reasoning. Using the new notion of inductive lvalues, our technique can handle loops where previous techniques fail, and it unifies acceleration for arrays and scalar variables by regarding scalars as arrays of dimension 0. Moreover, our approach uses λs instead of quantifiers. Then the resulting SMT problems can be solved via lemmas on demand. An empirical evaluation of our implementation in the tool LoAT shows the power of our approach.

ABSTRACT. The fluted fragment lacks the Craig Interpolation Property. In this paper we establish a weakened form of interpolation. Given an entailment in the fluted fragment, we distinguish predicates that only take an argument sequence starting with $x_1$ from those that do not. A predicate of the former kind is allowed to appear in a weak interpolant only if it occurs in both the premise and the conclusion; and any predicate of the latter kind can be used in a weak interpolant no matter whether it is in the shared signature. Our proof also shows that the weakened interpolation holds in every finite variable subfragment of the fluted fragment. In addition, this work provides a generalization of A. Herzig's translation of the ordered fragment, as well as a new proof of the finite model property of the fluted fragment.

ABSTRACT. The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique,owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process—a critical phase wherein the algorithm attempts to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 2,957 instances, primarily drawn from the HWMCC collection, demonstrates the efficacy of our approach. When implemented on rIC3, our method solves 28 more cases than the baseline, and on IC3Ref, it achieves an improvement of 14 additional solved instances. Our method improves the PAR-2 score by 170.04 and 71.43 seconds for rIC3 and IC3Ref, respectively.

ABSTRACT. At the core of modern electronic design automation (EDA) tools is rewriting: a mechanism by which local transformations are iteratively applied to circuits to make them faster and more efficient. These rewrites are crucial for producing high-quality hardware, and they often depend on extremely delicate conditions, relating, for example, to the widths of the various bitvectors involved. As such, it is both desirable and difficult to prove them correct. Prior work has studied the correctness of parametric-bitwidth rewrites in the context of software compilers and SMT solvers, but those approaches struggle to handle rewrites that have multiple bitwidth parameters, as are commonplace in EDA. We propose a language for expressing these multi-width parametric rewrites and provide a translation into equivalences in modular arithmetic. We then show how these equivalences can be automatically and efficiently proved using equality saturation over a set of carefully chosen axioms, and finally reconstructed automatically as theorems in Isabelle. This process is implemented in a tool called ParaBit. Using benchmarks from prior compilers work and from industrial EDA tools, we demonstrate that ParaBit can solve a class of problems that are intractable using existing techniques.

ABSTRACT. Formal hardware verification ensures that a design satisfies its specifications, but writing these specifications requires substantial manual effort. Specification mining automates this process, and existing work has their own merits. The classic approaches rely on pre-defined templates, which have limited expressiveness and lack formal correctness guarantees. But recent years have seen the emergence of using formal program synthesis for specification mining, which provides general and correct specifications but struggles to scale to complex designs. In this work, we present MAPminer, a parallel framework for synthesis-based hardware specification mining. MAPminer exploits its novel algorithm based on the Maximum Universal Subset and partitions the synthesis problem into efficient sub-problems. These sub-problems are automatically scheduled across multiple threads for parallel synthesis. Experimental results show that \name produces more effective assertions, improving verification coverage while reducing assertion size.

ABSTRACT. SystemVerilog remains one of the most widely used languages for designing and verifying digital circuits. Despite its importance, the SystemVerilog standard suffers from ambiguities, which can lead to inconsistent implementations and portability challenges. Formal methods can provide precise semantics to address these issues. We focus on SystemVerilog's mechanism for determining the bit-width of each expression that appears in a design. This is surprisingly subtle because an expression's bit-width can depend on both its children \emph{and} its parents. First, we develop a Rocq formalization of the current SystemVerilog specification. We then construct a bidirectional type system that captures the context-dependent nature of SystemVerilog expressions and prove it equivalent to our formalization of the existing IEEE standard using Rocq. We provide a reference implementation that determines bit-widths in linear time and prove its correspondence to our system, also in Rocq. Based on these results, we propose revisions to the text of the standard that reduce redundancy and improve precision.

ABSTRACT. Side-channel attacks are a major threat to the security of cryptographic schemes and digital signatures. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.

ABSTRACT. This paper introduces SpecIBT, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). SpecIBT is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and set the SLH misspeculation flag. We formalize SpecIBT as a transformation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline.

ABSTRACT. We present a shallow embedding of fractional separation logic in Isabelle/HOL, based on fractional separation algebras with unbounded fractions. To support flexible ownership splitting and recombination, we use nominal labels that enable systematic distribution and collection of fractional permissions across separating conjunctions. The logic is integrated into a verification condition generator that automates substantial parts of fraction arithmetic and label reasoning, significantly reducing manual proof effort. As a backend, we connect the framework to Isabelle/LLVM, enabling the verification of executable LLVM code. As a case study, we verify a parallel matrix-vector multiplication. The example illustrates recursive reasoning, parallel writes to disjoint segments of the result vector, and shared read access to the input vector via fractional permissions.

ABSTRACT. Separation Logic is an established formalism for deductive verification of heap-manipulating programs. Proofs of symbolic heap entailment, an analogue of the ordinary logical implication, are amongst the most common reasoning steps in Separation Logic, and many existing heap verifiers provide automation for discharging valid heap entailments. We observe that existing techniques for automating entailment proofs in foundational Separation Logic-based verifiers embedded into provers such as Rocq, suffer from three main drawbacks: poor performance due to metaprogramming overhead, limited expressivity (missing dependent types) due to the type-term stratification and restricted extensibility in computational reflection To address these, we propose lazy proof automation---an approach to entailment proofs inspired by translation validation. Our key idea is to implement an entailment checker as a combination of a (1) an efficient but untrusted prover, suitable for fast-paced interactive proofs, and (2) a proof reconstruction procedure that consumes the prover's trace to produce a certificate of entailment validity that can be checked in a post-hoc fashion. We implemented these ideas in Yolo---a generic and extensible heap entailment prover built in Lean. We instantiate Yolo for two Lean-embedded Separation Logics and show its practical benefits, both in terms of user experience and proof-checking speed, compared with the automation available in state-of-the-art foundational Separation Logics.

ABSTRACT. Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Choreographies formalize the way many practicioners think about distributed protocols, and are a natural framework in which to prove properties of such protocols. Previous work has introduced a Hoare calculus for reasoning about choreographies. In this article, we show how a formalization of that work in a theorem prover revealed several issues with the pen-and-paper development. We discuss the extent to which these issues can be fixed, and conclude with some considerations on the need for more formal verification of research results.