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