
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. 


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. 


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. 


Milad Ketab Ghale Haji Ali Proof Engineer 
Long ago Milad divorced the mysterious TRUTH and sided with proofobjects. He became mindful of practicality as much as the correctness. After his PhD at ANU, he join TS doing proof engineering where he can practice the best of formal method techniques and tools for the sake of both the correctness and practicality. Currently, his work concerns the CASE project where he is validating a translation of seL4 system initializer from its Isabelle specification into CakeML language.. 


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. 


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. 


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


Zoltan Kocsis Proof Engineer 
Zoltan, a nonstandard analyst by training, works on the correctness proof for the seL4 kernel. 
