I am a postdoc in Prof. Timothy (Mothy) Roscoe’s group, in the Systems Group of the Department of Computer Science at ETH Zürich.

My background is in formal methods. I did my PhD at MIT in Prof. Adam Chlipala’s group, working on machine-checked end‑to‑end proofs about software-hardware stacks.

Now, as a postdoc in Mothy’s group, I am excited to learn about real operating systems and to apply formal methods to systems research.

Currently, I am leading the development of Sockeye, a domain-specific language and analysis tool to formalize and analyze hardware reference manuals of Systems-on-a-Chip (SoCs). It supports both automated bug finding as well as proving security properties about hardware platforms and their configurations, and comes with a growing library of specifications of a diverse range of hardware platforms, unifying code by more than a dozen contributors.

Past Projects

• I invented Live Verification, a software development method that enables programmers to formally verify their code at the time they write it. After each line of code that the programmer wrote, the tool displays a concise summary of everything it knows about the current state of the program, which can inform the programmer on what the next line of code should be, and once the programmer is done writing a function, the displayed summary of the symbolic state can be turned into a proof of a postcondition. I implemented the tool in the interactive theorem prover Coq (now called Rocq), so in order to trust proofs about programs written in it, one only needs to trust the language semantics and Coq’s proof-checking kernel, but not the implementation of the Live Verification tool itself.
• Trouble combining undefined behavior and nondeterminism? ➔ Try omnisemantics!
  While working on Bedrock2, my colleague Andres Erbsen and me came up with a style of programming language semantics that we think works much better in the presence of undefined behavior and nondeterminism than using traditional smallstep or bigstep operational semantics would. A little later, our advisor Adam Chlipala chatted with Arthur Charguéraud and they found out that he had discovered the same style of semantics as well, but was using it for functional languages, while we were using it for imperative languages. Together, we wrote a paper about it, or if you prefer just a short introduction, you can also check out this blog post.
• With my colleague Andres Erbsen, I developed Bedrock2, a program logic to formally verify systems code.
• I developed formal RISC-V ISA semantics in Coq that support a wide range of use cases.
• I wrote a formally verified compiler in Coq from a small subset of C (as specified by Bedrock2) to RISC-V machine code (as specified by riscv-coq). It enabled several research projects of me as well as of my colleagues, including end-to-end systems proofs that cross the software-hardware boundary, a formally verified cryptographic server, proofs about a trap handler combining C and assembly, a compiler extension to support proving running-time bounds, another extension to prove cryptographic constant time, and it also served as a case study to illustrate the advantages of omnisemantics. I wrote up its design considerations in Chapter 3 of my thesis.
• I was visiting Dr. Toby Murray at the University of Melbourne for 10 weeks to work on information flow control proofs for C.
• For a six months master thesis internship, I was working with Prof. Andrew Appel’s group at Princeton, improving the proof automation tactics of their Verified Software Toolchain. (VST), and using it to verify the AES encryption implementation of mbed TLS.
• During my master’s at EPFL, I was working with Prof. Martin Odersky’s Scala lab on the Dependent Object Types project, a formalization of the core of Scala’s type system, writing proofs on paper and using the proof assistants Twelf and Coq.
• For a class project at EPFL, I contributed to the function termination checker of Leon, a tool for verification and synthesis of Scala programs by Prof. Viktor Kuncak’s group.
• While working at the Scala lab, I contributed to dotty, a new Scala compiler serving as a research platform to investigate new language concepts and compiler technologies for Scala, which eventually became the compiler for Scala 3.
• For my bachelor thesis, I designed, explored and implemented a simple structurally typed language in PLT redex.

Publications

Preprints, Theses, Reports

Education

• September 2024: PhD in Computer Science at MIT with Prof. Adam Chlipala’s Programming Languages and Verification Group
• April 2017: MSc in Computer Science from EPFL in Lausanne, Switzerland
• July 2013: BSc in Computer Science from EPFL

Industry Experience

• Summer 2021: At Google Research, worked on the Silver Oak Project, using Bedrock2 to formally verify drivers for peripherals used in the OpenTitan root of trust, and connected software correctness proofs to hardware correctness proofs
• Summer 2019: Worked with Rustan Leino at Amazon’s Automated Reasoning Group on a prototype rewrite of Amazon’s S3 Encryption Client in Dafny, a verification-aware programming language. Wrote and proved specifications for software interacting with real-world systems such as Amazon’s S3 storage service
• Fall 2015: 6 months Software Engineering Internship at Netcetera AG, Berne, working in a scrum team, developing a Web Application with a Java/Oracle DB/Spring backend and an AngularJS/TypeScript frontend
• Summer 2012: Java Internship at Accenture in Bangalore (India), developed a web interface with JSF/Enterprise JavaBeans monitoring hundreds of servers and databases