FMOℤ 2026 Program

Slides

Abstracts

Rajeev Gore and Cormac Kikkert (Monash University and Cormac Kikkert Research)

Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover ksp as an oracle. Our experiments using our C++ implementation cegarboxpp of CEGAR-tableaux show that: (1) cegarboxpp with RECAR SAT-shortcuts is not competitive and (2) cegarboxpp using ksp to provide SAT-shortcuts is superior to both cegarboxpp and ksp, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.

Thomas Haines (ANU)

Vestigial Vulnerabilities That Haunt Verified E-Voting Systems

slides

Verifiable electronic voting systems represent one of the most ambitious applications of modern cryptography — designed, audited, and refined to give voters confidence that their ballots are counted as cast. Yet even after a system’s core protocols have been scrutinised and its known vulnerabilities patched, something troubling remains: a class of weaknesses that survive the audit process and linger undetected in production deployments.

Drawing on recent work by Haines and Rose (Vestigial Vulnerabilities in Deployed Verifiable E-Voting Systems, 2025), this talk examines two persistent categories of vulnerability found in real-world e-voting systems. We explore why these weaknesses consistently escape detection despite rigorous review processes, and ask an uncomfortable question: if the best-audited systems in the world still harbour these issues, what does that say about our verification methodology?

Miki Tanaka (UNSW)

Pancake at Trustworthy Systems Group - Updates

Pancake is a verification-friendly, imperative low-level language for systems programming, which the Trustworthy Systems group at UNSW has been working on to produce verified LionsOS components. Pancake is now mature enough for our systems engineers to take up and port various components originally written in C to Pancake.

In this talk, we report on various recent updates on Pancake and its roadmap, in the broader context of LionsOS. We’ll cover the progress and plans for the general Pancake language extensions and compiler improvements as well as verification of programs written in Pancake, in particular device drivers, both via interactive theorem proving and SMT-based tools.

We’ll highlight the SMT-based approach via Pancake-to-Viper transpiler as a way towards TS’s vision of making verified software the standard for security- and safety-critical systems, aiming to make software verification more scalable and less expensive.

Rihui Wu (UNSW)

Adding support for memory barriers in Pancake

slides

Pancake is a system programming language with a formally verified compiler down to machine code, and has been successfully deployed for driver development in the seL4-based LionsOS operating system. However, for low-level system constructs like memory barriers, currently it requires making foreign function interface (FFI) calls to C. We describe the design of integrating memory barriers in the language and discuss its semantics.

Yan Liu, Alex Potanin (ANU)

CoreFi: An Orchestration Language for Embedded Systems — Bridging Implementation to Specification

slides

Establishing the correctness of concurrent systems has been approached from two directions historically: top-down, where global specifications are projected into local implementations, such as choreographic programming, and bottom-up, where global specifications are extracted from implementations for verification. Neither direction has found a satisfactory answer, especially when computation and communication are deeply intertwined and participants share state—as is common in embedded systems. We present CoreFi, a Communicating Sequential Processes (CSP)-inspired orchestration language that bridges low-level implementations (e.g., C) via computation events and top-level specifications via channel communication (with bounded buffers) and process composition, opening the door to automated formalisation and verification of the full implementation. CoreFi is short for Core Language of Fiducia, where the latter pursues secure by design through language-based information flow security.

Junming Zhao (UNSW)

A Rely-Guarantee + Separation Logic for Verifying Microkit-Based Systems

slides

Microkit-based systems on top of seL4 (such as LionsOS) have a static architecture: components fixed at build time, memory-region mappings declared up front, communication channels predefined. We’re developing an RGSep-style logic for this setting. The current basis is local rely-guarantee reasoning, with each shared region carries a precise invariant.

The development is in Isabelle/HOL over the seL4 trace monad, with frame and hide rules currently mechanised. The talk will design choices and the path toward verifying real LionsOS subsystems.

Vincent Jackson (UNSW)

SecRGSep: A General Logic for Information Flow Security

slides

In this talk, I will outline my work on a general framework for relational information-flow security logic, based on RGSep. I will show how to give security conditions directly in a relational semantics, rather than via a trace of leaks. This presentation leads to a simple condition to identify when atomic commands leak or declassify information. In addition, in this setting, declassification has a natural encoding as concurrent await. Then I will show that, when non-determinism does not leak information, the atomic security properties naturally generalise to show the security of the entire program. Lastly, I will show how to allow information-flow security and separated state to interact. In particular, I show how to accommodate programs which contain leaky operations on local, separated data. These results are formalised in Isabelle/HOL.

Chelsea Edmonds (UWA)

Proof Engineering in Isabelle/HOL: From Combinatorics to Rely-Guarantee

slides

Formalisation using proof assistants is often primarily viewed as a way to guarantee correctness, however the process itself can also lead to deeper insights and the development of frameworks and tooling to support future research efforts. Proof engineering is a critical part of supporting this process, particularly as formalisation becomes more accessible and libraries rapidly grow. In this talk I’ll give an overview of two examples of proof engineering from formalised mathematics and program verification. I’ll begin with an example from combinatorics, highlighting the effective use of locales to develop a modular, reusable formal proof technique framework. I’ll then shift to focus on the role proof engineering played in some recent joint work on developing a coinductive foundation for rely-guarantee reasoning in Isabelle/HOL, which arguably provides simpler formal proofs than its inductive counterpart. In particular, this will highlight how the proof engineering process was also valuable in developing the main theoretical insights of the work.

Rob Sison (UNSW)

Clearing roadblocks to Time Protection verification for seL4

slides

This talk will present the theory and practice underpinning recent advances in our ongoing efforts to verify time protection for seL4 at UNSW’s Trustworthy Systems group. Thanks to a rethink of our use of ghost state to specify that seL4’s memory accesses are well partitioned and that this remains true down to its C implementation via refinement, we have eliminated the main cause of the project’s previously large number of breakages to seL4’s existing Isabelle/HOL proofs. After explaining our change of strategy and its impacts, I will present the progress and results achieved by our verification efforts so far, and thus our updated roadmap towards the first proof that any OS implements time protection for systems that demand complete isolation of security domains from one another. I will also remark on where we stand and next steps forward to formalise and verify new time-protected cross-domain communication mechanisms we have implemented in seL4 on RISC-V Cheshire. In particular, these mechanisms must ensure one-way communications are truly one way, without permitting any timing channels in either (but most importantly, the backwards) direction.

Toby Murray (University of Melbourne)

Beyond ‘I Told You So’: Formal Methods in the Age of AI

AI is suddenly doing useful things. It can write code, find vulnerabilities, propose patches, and even construct machine-checked proofs. We might be tempted to view the oncoming storm of AI-discovered security vulnerabilities as vindication: we were right all along to demand rigorous standards of software correctness and security. But “I told you so” is hardly a research agenda. The more interesting question is how formal methods researchers should rise to this moment of disruption in which we find ourselves.

Some software verification tasks will become much more important, such as verifying the correctness of software patches​ rather than entire software systems. I’ll explain how formal methods provide the infrastructure for performing assurance at AI-scale. As formal methods are increasingly wielded by AI agents, we might also change our ideas about which formal methods are most usable. Interfaces to formal methods tools will become important objects of research. This is already happening as research teams and companies race to build agentic formal methods. Finally, the correctness and security of AI-based systems will become increasingly important. I’ll explain how this opens new opportunities to rethink how we verify AI-based systems. This includes emerging assurance methods for agentic AI, which may leverage AI-usable formal methods as a substrate for agents to justify the safety of their actions.

Aaron Bembenek (University of Melbourne)

Automated Reasoning Is Inherently Deeply Neurosymbolic

slides

Traditionally, automated reasoning algorithms (like those underlying SAT solvers) have been symbolic, perhaps augmented with learned heuristics; recently, there has been much interest in building reasoning tools that combine LLMs and symbolic components. In this talk, I argue that automated reasoning is neurosymbolic in a deeper and more fundamental sense than these existing integrations capture. My argument is part conceptual: I present an expanded view of the nature of computation that locates automated reasoning as especially well suited for neurosymbolic evaluation. My argument is also part technical: building on the conceptual lens, I propose Neurosymbolic Transition Systems, a computational framework that can be used to lift symbolic automated reasoning algorithms to neurosymbolic versions. I believe that these insights can be the foundation of future automated reasoning systems that—by combining logic and “intuition” in a principled way—are more effective and usable in practice.

Christine Rizkallah (University of Melbourne)

Towards Facilitating Verification across Language Boundaries

slides

Software verification is essential for building secure and reliable systems. Landmark projects such as the verified seL4 microkernel and the verified CompCert compiler have pushed the boundaries of what is considered feasible in our field. However, many critical software components remain unverified, and important properties beyond the correctness of sequential code still require attention. Verifying such systems using existing brute-force techniques would be infeasible. Instead, my research focuses on reducing the manual effort required to verif software within interactive theorem provers, without compromising performance or trust.

In this talk, I will present several lines of work that advance this goal across various settings. I will first briefly start by demonstrating how our Cogent language, through its uniqueness type system and certifying compiler, facilitated the development of trustworthy file systems. While safe languages such as Cogent, Swift, and Rust prevent memory-safety errors and support refinement from functional code into efficient imperative code, they often limit low-level control over memory layouts.

To address this limitation, I will present our declarative data-layout specification language extension, Dargent, which enables Cogent programmers to regain fine-grained control over memory layouts. This approach trivialised the verification of low-level systems components, such as device drivers, down to the bit level.

Even with such extension, safe languages still limit expressivity and therefore, typically rely on foreign-function interfaces to interoperate with performance-critical components written in unsafe languages such as C or unsafe Rust, where formal verification remains more challenging. Since real-world systems span multiple programming languages, we have ongoing efforts that aim to ease verification across programming language boundaries. In particular, we demonstrate how separation logic can be used to discharge uniqueness-type obligations, bridging reasoning principles between type-safe components and components where safety requires manual proofs.

Finally, I will briefly outline ongoing work on easing the cost analysis of lazy functional programs and on developing logical frameworks that extend safety guarantees to information-flow security, including for concurrent systems.

Nicholas Coughlin (UQ - DSTG)

Translation Validation for LLVM’s Loop Optimisations

Compilers are a foundational component of modern software development, translating high-level programming languages down to executable representations. Despite performing such a critical role, their correctness properties are widely underspecified, and their implementations have been repeatedly shown to be incorrect. To provide greater compiler correctness guarantees, we develop a translation validation technique for an industry strength compiler, LLVM, by which the correctness of a compilation can be automatically evaluated. Our approach builds on recent results in the space of safety property verification. In this talk, we describe how we leverage these recent results, based primarily on abstract interpretation techniques and various insights into LLVM’s implementation.

Peter Höfner (ANU)

Towards an Algebraic Theory of Pushdown Automata and Turing Machines (Joint work with Yi Yao)

slides

Kleene algebra, as shown by Dexter Kozen, provides a sound and complete equational theory for regular languages, with decidability inherited from the equivalence of nondeterministic finite automata and regular expressions. A natural question is whether this elegant connection can be lifted to more expressive computational models, such as pushdown automata and Turing machines. In this talk, I present initial ideas towards an algebraic framework for pushdown automata based on a trace model, in which elements of the algebra are sets of sequences interleaving input symbols with stack configurations. I describe how this structure gives rise to a Kleene algebra, how pushdown automata and context-free grammars can be encoded within it, and what the decidability landscape looks like from this algebraic point of view.

Ali Nosherwan Hamed (ANU)

Asynchronous Hyperlogics

slides

Computational processes can be represented by models of an appropriate temporal logic, and results about the logic can be used to verify that the processes run as expected. This is of special concern for concurrent processes that can interleave in complex and unpredictable ways. I shall present my work on Asynchronous HyperCTL* — a logic that can express hyperproperties, such as security policies, over branching structures and which has an asynchronous semantics, i.e., it can represent system traces proceeding at different relative speeds. The expressive power of such logics allows for finer distinctions between models of computational processes and can be used to improve how they are classified, e.g., models might be bisimilar, even though one stutters. Asynchronous hyperlogics can therefore be used to study security policies in more realistic setting.

Cezary Kaliszyk (University of Melbourne)

Modern Proof Formalization with Strong Automation and LLMs

slides

This talk compares several lines of LLM-assisted autoformalization across Megalodon, Isabelle/HOL, and Mizar, spanning different mathematical domains and proof-assistant cultures. The Megalodon work studies decentralized proof development with multiple LLM-based coding agents, using a simulated bounty marketplace in which agents propose lemmas, assign proof obligations, invoke tactics, inspect proof states, and compete to complete verified formal developments. The Isabelle/HOL work emphasizes large-scale textbook formalization using a sorry-first workflow and extensive automation, while the Mizar work highlights declarative proof style, library alignment, and the formalization of surreal numbers. Taken together, these projects show that autoformalization is not a single uniform task, but a family of workflows shaped by formal language, proof style, automation, library structure, and the ways in which LLM agents interact with proof assistants.

Matthew Daggitt (UWA)

Formal Verification of Neural-Cyber-Physical systems

slides

Formal verification of neural-cyber-physical systems, such as drones, medical devices and robots that are either fully or partially controlled by neural networks, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the “cyber” and “physical” behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting neural model.

In this talk I will discuss recent work by myself and collaborators on methodologies for verifying such systems. As part of this, I will discuss the Vehicle framework, an implementation of our ideas, which provides a functional, domain-specific language for specifying, training, and verifying neural components. Vehicle is then capable of exporting verified neural specifications to ITPs such as Rocq, Isabelle/HOL, Agda and Imandra in which the larger cyber-physical system can then be reasoned about.