I am Rao Xiaojia(饶晓嘉). I am currently an independent researcher in theorem prover mechanisations and formal verification, focusing on the WebAssembly spec in Rocq and Lean.

I have previously completed my PhD in Computer Science at Imperial College London, advised by Philippa Gardner and Conrad Watt.

Prior to my PhD studies, I studied mathematics at University of Cambridge during 2015-2019.