Hi! I am a PhD student in Prof. David Basin's Information Security Group at ETH Zürich.

My research focuses on the formal verification of systems software, especially operating systems. With my collaborators, I am exploring how to verify an OS from the perspective of a user-space process. This results in a specification that is effectively a contract for user-space software. In contrast to verified systems that focus exclusively on security properties, a system with such a process-centric specification will be able to support the construction of end-to-end verified software stacks.

I primarily use the code verification tool Verus in my research but I find that for certain abstract reasoning tasks, interactive theorem provers (ITPs) like Isabelle/HOL are more convenient. Because of that, I am investigating methods of enabling sound interoperability between these tools, with the goal of making heterogeneous verification methodologies practical.

To support proof engineering efforts in Verus, I develop verus-find, which can find all Verus functions and lemmas matching a user-provided pattern, either in the standard library or some other project. It is available as a CLI tool and as a web version for Verus' standard library.