A very special thank you to the seL4 2026 Program Committee! Nick Spinale Independent Computer Security Researcher Nick Spinale Independent Computer Security Researcher I am an independent computer security researcher based in Portland, Oregon. My interests include operating systems, formal methods, programming languages, and reverse engineering. These days, most of my time at work is spent hacking on and around seL4, the formally verified microkernel. Right now I’m working on binary verification and seeding the seL4 userspace ecosystem with support for the Rust programming language. I offer my consulting services through Colias Group, LLC. Martin Dehnel-Wild Chief Scientist Kry10 Lesley Rossouw Operating Systems Engineer UNSW Lesley Rossouw Operating Systems Engineer UNSW Computer engineer with an interest in operating systems, cybersecurity, microkernels, virtualisation, electronics, computer architecture and hardware design Leigha Vanderklok Embedded Systems Engineer II DornerWorks Ltd. Juliana Furgala Technical Staff MIT Lincoln Laboratory Juliana Furgala Technical Staff MIT Lincoln Laboratory Juliana Furgala is a technical staff member in the Secure Resilient Systems and Technology Group. Currently she is researching secure and recoverable satellite systems. Interested in the pursuit of technology built with security in mind, she aims to develop lasting technology that can stand the test of adversaries, not just the test of time. Her recent published research focuses on the needs of embedded and real-time systems. Furgala received her MS degree in cybersecurity in 2024 from Georgia Institute of Technology and her BS degree in computer science in 2019 from Tufts University, where she also minored in history with a focus on global premodern women’s history. In 2018 she interned at MITRE, where she began her journey of studying satellites. There she developed technology to enable GPS receivers to directly communicate satellite information with each other without needing further satellite access, assuming that one receiver has prior data stored. Gernot Heiser Lead Trustworthy Systems Group Gernot Heiser Lead Trustworthy Systems Group Gernot leads the Trustworthy Systems group. He aims for principled, fundamental solutions to real-world problems, meaning his activities range from fundamental research to technology transfer and real-world deployment. He sees research-driven teaching as a core part of this agenda, challenging students to grow, recruiting them into research and sending them out into the real world as ambassadors of TS and its technologies, and helping to advance the growth of industrial cybersecurity capabilities. Most of his work is on seL4 and related technologies, and evangelising them is a significant part of his activities. David Hardin Associate Director Loonwerks David Hardin Associate Director Loonwerks David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as memory-safe programming languages. He is currently Chief Technologist for Trusted Methods in the Applied Research and Technology organization at Collins Aerospace, where he has served as Principal Investigator or Researcher for several U.S. DoD Research and Development programs. He most recently contributed to the DARPA Cyber-Assured Systems Engineering program (CASE). He is the editor of the book Design and Verification of Microprocessor Systems for High-Assurance Applications (Springer 2010), and a co-author of The Real-Time Specification for Java. He is author or co-author of more than 75 peer-reviewed publications, and is an inventor or co-inventor on 15 U.S. patents. In 1999, Dr. Hardin co-founded aJile Systems, a startup company focused on real-time and embedded Java technology, and served as aJile’s Chief Technical Officer from 1999 to 2003. Dr. Hardin was selected as a Rockwell Engineer of the Year for 1997 for his contributions to the development of the world’s first Java microprocessor. His academic career includes BSEE and MSEE degrees from the University of Kentucky, and a Ph.D. in Electrical and Computer Engineering from Kansas State University, in 1989. Dr. Hardin is a proud native of the Commonwealth of Kentucky, and is a Kentucky Colonel. David Cock Head of Verification Neutrality David Cock Head of Verification Neutrality David is an early contributor to the seL4 microkernel, having contributed both the first C implementation and seminal formal-verification work. He holds a Ph.D. from the University of New South Wales where his research included probabilistic and non-functional properties of seL4 such as side channels. As a senior researcher at ETH Zurich, he also led the team that built the Enzian research computer. Corey Lewis Engineer Proofcraft Corey Lewis Engineer Proofcraft Corey was a senior proof engineer and the lead engineer for verifying multi-core seL4. During his time at TS he has been involved in a wide variety of projects to do with seL4. These include developing the original CapDL translation tools, helping complete the information flow proofs, and contributing to the verification of the seL4 MCS extensions. His research interests include formal methods, functional programming, and program verification. Corey now works at Proofcraft. Adam The National Cyber Security Centre Lucy Fletcher Secure Kernel Engineer Apple Robbie VanVossen Embedded Systems Engineer DornerWorks Ltd. Robbie VanVossen Embedded Systems Engineer DornerWorks Ltd. Mostly have done work with separation technologies, especially Xen and seL4.
