ABSTRACT. Finite multisets (also known as bags) are a fundamental data structure that generalizes finite sets to record the elements' multiplicities. In the Isabelle proof assistant, finite multisets are defined as the subtype of functions from elements to natural numbers consisting of functions that return non-zero multiplicities for finitely many elements. This representation is negative: the elements occur to the left of the function arrow. To allow (co)datatypes to (co)recurse through multisets, an alternative positive representation as quotients of finite lists of elements modulo permutations is used. Using Isabelle, we define two orthogonal generalizations of multisets and the respective positive and negative representations. First, we view countable multisets either as functions from elements to extended natural numbers that return non-zero multiplicities for countably many elements or, alternatively, as quotients of lazy lists modulo infinitary permutations. Second, we view weighted sets either as functions from elements to optional weights from a well-behaved algebraic structure that return None for all but finitely many elements or, alternatively, as quotients of element-weight lists modulo permutation and regrouping by element. For both types, we establish the necessary functorial structure to support (co)recursion and exemplify this support in two case studies.

ABSTRACT. We present IsaSearch, an automatic, self-contained system for natural-language search over Isabelle developments. The system extracts formal Isabelle content, translates it into informal descriptions using large language models, and indexes these descriptions for semantic search. At search time, the system optionally applies query expansion to improve robustness against short or imprecise queries. The system supports different Isabelle and Archive of Formal Proofs (AFP) versions, language models, and prompts without changes to the implementation. We evaluate the approach by searching the AFP using benchmarks derived from Wiedijk's "Formalizing 100 Theorems". The results show that semantic search over generated natural-language descriptions of Isabelle content is effective.

ABSTRACT. This paper reports on the design, content development, tooling, and first-year experiences of using the Isabelle Platform for a compiler construction course with fourth-year engineering students at Université Paris-Saclay/Polytech. The course covers formal grammars, several parsing techniques, syntax-directed translation, and code generation for a fragment of a processor instruction set architecture (ISA). While formal proofs remain out of scope for this class, the Isabelle platform still offers numerous advantages: it is easy to install across major operating systems, features an IDE with relevant SML libraries, and can be set up to work with Lex/Yacc-like tools. Furthermore, we describe how Isabelle’s document-preparation facilities (via Isabelle/DOF) were deployed to provide students with a consistent, formally checked, and practically rewarding learning environment for both specification and implementation activities. Finally, we share observations and lessons learned from the initial run of this class within the fourth-year computer science program.

ABSTRACT. As the software industry shifts toward memory-safe languages, automated reasoning pedagogy must evolve to bridge the gap between industrial practice and formal verification. We explore the integration of AutoCorrode, a framework for reasoning about imperative Rust-like code within Isabelle/HOL into computer science curricula. We demonstrate its utility through a worked example of an iterative Fibonacci function, illustrating how students can apply Hoare logic and separation logic to modern imperative paradigms.

ABSTRACT. We report on the design and implementation of a verification condition generator (VCG) for fractional separation logic in Isabelle, developed primarily using Eisbach with lightweight Isabelle/ML extensions. Rather than focusing on the underlying logic itself, this paper concentrates on the engineering of the proof automation infrastructure. We present a modular VCG architecture based on explicit normalization, controlled rule applica- tion, frame inference, and configurable verification-condition handling. During the implementation effort, several reusable proof-engineering patterns emerged, including combinator-style Eisbach methods, dispatch based on subgoal shape, configurable failure behaviour for debugging and strict modes, and an orthogonal mechanism for deferring verification conditions. In addition, we describe auxiliary tools developed during the project, such as a focused goal deferral mechanism (SDefer) and a theorem-search tool for named theorem collections. While the implementation targets a specific separation logic, many of the presented techniques are largely independent of the underlying logic and may be useful for Isabelle automation more broadly.

ABSTRACT. We present an Isabelle/HOL mechanisation of rely-guarantee reasoning combined with separation logic, developed on the seL4 trace monad: an Aczel-style trace model that makes environment interference first-class. We follow Feng's local rely-guarantee (LRG) because its frame rule fits the seL4 Microkit framework we target: a static-architecture setting in which components, their memory-region mappings, and the communication channels between them are fixed at build time. The development so far has: (i) LRG's frame and hide rules, mechanised over the trace monad's primitives, sequential composition, and while loops; (ii) an n-ary parallel composition rule; and (iii) a three-component Microkit case study (a producer/filter/consumer pipeline over shared memory regions) composed by the n-ary parallel rule.

ABSTRACT. This talk will present two case studies on verification interfaces at both ends of the seL4 operating system kernel's bulk of formal specifications in Isabelle/HOL. Reaching deep into the concrete depths, our efforts to prove that seL4 enforces time protection, the absence of timing leaks through microarchitectural state, rely entirely on a new hardware–software contract. Meanwhile, up where verified user-level programs would need to rely formally on a suitable abstraction of seL4's system call behaviour, there stands a long-unbridged kernel–userland gap: what developers would expect from reading seL4's reference manual is not quite yet what's been proved. We will examine how the urgent need to clarify both interfaces arose and what we are doing about it at UNSW, offered as data points for discussion on what it can take to provide a trustworthy body of software through formal methods and mechanised verification in Isabelle.

ABSTRACT. This is a brief and mostly LLM-written (but human checked/rewritten) report on my recent experience with agentic autoformalizaton using Isabelle. We discuss the problems encountered and solutions developed during an LLM-assisted autoformalization of Munkres’ Topology (§§12– 85) in Isabelle/HOL. The project (200,000+ lines, 4,000+ commits, described in [1,2]) has surfaced a range of issues that we believe are representative of large-scale LLM–ITP interaction. The proposed talk at the workshop will likely discuss some of these issues and perhaps more.