I’m a postdoctoral researcher at ETH Zürich in the programming methodology group where I work on the performance and methodology of formal verification.
Previously I was a PhD student at the LMF where I developed Creusot, a state-of-the-art verifier for Rust based on translation to pure, functional programs.
Using Creusot, I explored how to push the scale and efficiency of verification, leading to the development of CreuSAT a verified, high-performance SAT solver, and Sprout a verified SMT solver.
Using Creusot, we developed an ergonomic methodology for verifying iterator-based code in first-order logic, including higher-order functions with side-effects like map.
In my previous life, I was a production engineer at Shopify, where I helped transition the core platform from to a novel sharded architecture, resilient to datacenter failures.