Associate Professor
School of Computing, Australian National University
Adjunct Professor, S3D, Carnegie Mellon University
Senior Visiting Fellow, Trustworthy Systems, UNSW Sydney
I design programming languages and verification techniques and tools that make software safe, secure, and verifiably trustworthy — across cyber security, trustworthy devices & systems, quantum computing, and software engineering.
My work spans secure and trustworthy systems, Rust and concurrency verification, quantum computing, and programming language design
Fiducia is part of a broader toolkit for developing secure and trustworthy embedded systems, providing information flow and liveness guarantees for critical deployments. Built on the Trustworthy Systems seL4 microkernel as a foundation for verified security properties.
fiducia-lang.github.ioMaking Rust's safety guarantees go further: view types for partial borrows that let the borrow checker accept more provably safe programs (formalised in Aeneas), and verification of concurrent and lock-free data structures using Iris and Verus.
Verified RustVerification of quantum programs, including embedding quantum program verification into Dafny and symbolic execution of quantum circuits. Our ESOP 2026 Distinguished Paper validates quantum state preparation programs.
Distinguished Paper AwardA secure general-purpose programming language using object capabilities and effects, developed with Jonathan Aldrich at CMU. Influenced CUE and Scala (see Impact).
wyvernlang.github.ioCurrent postdocs and PhD students. Solid border indicates primary supervisor.
View all current & past students (including undergraduates) and how to apply
Alex completed his PhD (submitted 2006, conferred 2007) on Generic Ownership, showing how type polymorphism can be used to provide ownership type support in any language. This approach has since been widely adopted by the Rust Programming Language as "lifetime parameters". He went on to demonstrate deep connections between ownership and immutability with the help of the Royal Society of New Zealand Marsden Fund (2008 - 2011), with a book chapter on Immutability outlining the core outcomes of this work.
After a full-year sabbatical at Carnegie Mellon University working with Professor Jonathan Aldrich, Alex created the Wyvern Programming Language - a novel general-purpose language designed from the ground up with security and usability as its primary goals. This produced numerous publications including work on type-specific languages and decidable typing for type members.
Since joining the Australian National University in 2022, Alex's research has centred on trustworthy systems and quantum program verification: the Fiducia language for verified embedded systems building on the seL4 microkernel, and the first embedding of quantum program verification into Dafny (OOPSLA 2025), with follow-on work on quantum state preparation recognised by an ESOP 2026 Distinguished Paper Award. He is a Permanent Member of IFIP Working Group 2.4, a Senior Visiting Fellow with the Trustworthy Systems group at UNSW Sydney, and leads the School of Computing's GenAI teaching deployment under the ANU–Anthropic partnership.
Alex's ownership type system research directly influenced how the Rust programming language implements its ownership and lifetime system - one of Rust's defining features for memory safety. The well-known "The Performance of Open Source Applications" book cites his research that revolutionised performance evaluations in Talos and similar systems.
The CUE configuration language, used widely within Alibaba's cloud, based its module system on Wyvern's design. Scala drew on our Wyvern research for its path-dependent types and type member mechanisms, and more recently adopted the capabilities-and-effects combination that Wyvern pioneered — see Scala's capture calculus, whose ideas originate in our paper Capabilities: Effects for Free (ICFEM 2018).
| Period | Grant | Amount |
|---|---|---|
| 2027 | Department of Defence (Australia) — Automated, Compositional and AI-Assisted Verification of Embedded and Cyber-Physical Systems with Fiducia | A$100,000 |
| 2026 - 2030 | NSF GOALI: SHF — Automated Verification and Validation for Quantum Software (US$850,000; co-PI; PI Liyi Li, Iowa State) | A$1,200,000 |
| 2026 - 2027 | Anthropic Claude API Credits for Teaching at SOCO (US$355,000; shared with Dr Ben Swift) | A$500,000 (in-kind) |
| 2026 | ANU CSS Tier 2 Learning & Teaching Grant: “Badges as a Complementary Performance Indicator” (shared with B. Pereira Nunes, A. Chen, B. Swift, B. Bergin, C. Martin, D. Guo, D. Campbell, A. Martin, P. Höfner, R. Shome, F. Muehlboeck, S. Okai-Ugbaje) | A$5,000 |
| 2025 - 2026 | Skykraft Industry Research Grant (multiple rounds) | A$30,000 |
| 2024 | DVCRI University Strategic Fund towards Centre of Excellence on Trustworthy Systems | A$36,000 |
| 2022 | ANU Startup Package Funding | A$500,000 |
| 2021 - 2023 | SHEADI Faculty Strategic Initiative PhD Scholarship | NZ$100,000 |
| 2020 - 2021 | Robonomics Network Research Grant | NZ$72,000 |
| 2019 | Kyoto University Visiting Professor Scholarship | NZ$20,000 |
| 2017 - 2018 | Oracle Corporation Research Grant | NZ$70,000 |
| 2012 | Mozilla Foundation Research Grant | NZ$15,000 |
| 2009 - 2011 | Royal Society of NZ Marsden Fast Start Grant | NZ$300,000 |
| 2009 | RSNZ ISAT Grant | NZ$5,420 |
| 2007 - 2016 | VUW University Research Fund (multiple rounds) | NZ$47,000 |
| Total (AUD) | A$2,880,830* |
* NZ$ amounts (grants starting 2021 and earlier) converted at 1 NZD = 0.81 AUD (September 2026).
