ABSTRACT. We describe our experience developing qrhl-tool, a theorem prover for verifying quantum cryptographic protocols, both in the post-quantum and the full quantum setting. The tool is built around quantum relational Hoare logic (qRHL), a relational program logic for reasoning about pairs of quantum programs in the style of game-based cryptographic proofs. We discuss the design choices underlying the tool: in particular, a hybrid architecture that delegates ambient-logic reasoning to Isabelle/HOL while qrhl-tool itself handles qRHL judgments and the program language; an advanced memoization mechanism (hashed computations) that enables efficient incremental proof checking; and a deliberate path towards a foundational implementation. We walk through a small worked example (the hardness of inverting f∘︎f given a one-way permutation f) to illustrate how these pieces fit together in practice. Along the way we highlight what we got right, what we got wrong, and which limitations (procedure parameters, local variables, runtime reasoning) we would approach differently if starting over today.

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. 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. Schröer et al. developed a verification infrastructure for rapid prototyping of automated verification techniques for probabilistic programs (PPs), which is based on the quantitative intermediate verification language HeyVL. In a nutshell, users encode programs, specifications, and proof rules into a single HeyVL program. The verification conditions obtained from such a HeyVL program are then discharged with SMT solvers or probabilistic model checkers. However, ensuring that a HeyVL encoding is correct can be subtle and error-prone, just like reasoning about PPs in general. In this paper, we develop mechanized foundations for writing formal correctness proofs for both HeyVL encodings and PP verification techniques that are grounded in the basics of probability theory. To this end, we formalize Markov decision processes (MDPs) - a standard model for assigning operational semantics to PPs. We construct suitable probability spaces for MDPs to ground them in probability theory. Furthermore, we develop least fixed-point characterizations of expected total costs of MDPs, which are useful for relating program logics or denotational semantics to an operational MDP semantics. We apply these characterizations to formalize sound weakest-precondition-style calculi for both partial and total correctness reasoning about the expected behavior of PPs with unbounded loops, nondeterminism, and conditioning. Finally, we develop a deep embedding of the HeyVL intermediate verification language. We apply the above machinery to prove the correctness of various existing HeyVL encodings. During that process, we improved the original HeyVL encoding of an invariant-based proof rule for loops. All of our results have been formalized in the interactive theorem prover Lean on top of mathlib.

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.