
Alison Felizzi OS Engineer 
Alison works on the seL4 operating system and infrastructure. 


Amirreza Zarrabi Proof Engineer 
Amir is researching operating system architecture, and multiserver architectures for OS design. He is currently on a break from his PhD to work as a proof engineer. 


Branden Robinson OS Engineer 
Branden is interested in all kinds of software development, and hopes to learn about verification and proof techniques as part of his work in the group. 


Corey Lewis Senior Research Engineer 
Corey is a senior proof engineer within the Trustworthy Systems group, and is currently the lead engineer for verifying multicore seL4. His research interests include formal methods, functional programming and program verification. He has also been interested in mathematically analysing graph models of large real world networks. 


Curtis Millar OS Engineer; Casual Academic, UNSW 
Curtis is interested in improving systems level security through advancements in platform architecture, tooling, and education. 


Damon Lee OS Engineer 
Damon is interested in operating systems, hardware, and the relationships between the two. 


Ed Pierzchalski Proof Engineer 
Ed is a proof engineer working on extending the seL4 proof to more architectures. 


James Ye OS Engineer 
James is interested in OS design and implementation. 


Kent Mcleod Research Engineer 
Kent is mostly concerned with lowlevel operating systems and drivers. 


Matthew Brecknell Proof Engineer 
Matthew is interested in formal verification of software, using mechanised theorem provers. His current challenge is figuring out how to rapidly, yet sustainably evolve large bodies of existing proofs to meet new requirements. 


Michael McInerney Proof Engineer 
Michael is learning the techniques to become a proof engineer. 


Miki Tanaka Senior Research Engineer 
Miki is mainly interested in formal verification techniques and their application to software systems. 


Mitchell Buckley Proof Engineer 
Mitchell has a formal education in mathematics and a research background in category theory, Hopf algebra and formalised mathematics. He now writes proofs that verify functional correctness of the seL4 microkernel. 


Qian Ge OS Engineer; UNSW 
Qian has just finished a PhD on eliminating timing side channels from seL4 with lightweight countermeasures. 


Siwei Zhuang Research Engineer 
Operating System internals, Device drivers and Embedded System Architecture. 


Sylvain Gauthier OS Engineer 
Sylvain is interested in working on and understanding UNIX systems and operating systems Kernels. 



Vincent Jackson Proof Engineer; Graduate Verification Engineer, UNSW 
Vincent is interested in proof theory, type theory, and theorem proving. 


Yanyan Shen Research Engineer 
Yanyan is currently researching how to improve the trustworthiness of commodity hardware through software to enable the verified microkernel to be used in situations previously needing an air gap. Multicore processors are used to provide redundancy and crosscore checking is employed to detect divergence caused by hardware faults. The aim is to increase the trustworthiness of a virtual air gap created by the microkernel, and thus systems running on COTS hardware. 


Yu Hou OS Engineer 
Yu is mainly interested in low level stuff such as operating systems and compilers. 


Zilin Chen Research Engineer; UNSW 
Zilin's research is into functional programming, type theory, formal verification, compilers, and Embedded DSLs. 
