Research
I aim to make computer systems, both software and hardware, more trustworthy. I focus on designing composable methods of reasoning, where proofs are constructed modularly and scale to large and complex situations.
On the software side, I have been developing a new foundational framework for the verification of distributed cryptographic protocols such as Multi-Party Computation.
On the hardware side, I am developing a framework for the composable verification of hardware leakage, specifically of processors such as the RISC-V core.
During my PhD, I used the Rocq theorem prover to formalize concepts from abstract homotopy theory.