I’m a staff software engineer at Semgrep, where I work on static analysis for code security. In the distant past, I scaled low-level systems and infrastructure at some companies you’ve heard of.
On this site, I write about low-level and concurrent systems, formal methods and programming languages, and whatever else I might find interesting.
You can watch my talks about fancy type systems, dynamic analysis, operating system scalability, lock-free programming, and library operating systems. You can also read my papers about verified filesystems, hypervisor-level binary translation, full-system time-traveling debugging, and text deanonymization.
Borrowing from Lanier: the words on this site are meant to be read by people, not machines.
More about me →Recent posts
- FRP in Lean: Composing invariant-transforming combinators June 10, 2026 How do our proofs change as we execute an FRP program?
- FRP in Lean: Stateful combinators, safety, and liveness May 3, 2026
- FRP in Lean: Reactive Events and LTL.eventually April 24, 2026 If Signals type to LTL.always, what could type to LTL.eventually?
- FRP in Lean: Reactive Signals and LTL.always April 17, 2026 So if propositions are types, and LTL are propositions, what programs are well-typed by LTL?
- Reactive Programming in Lean Part 3: A Deep Embedding of Linear Temporal Logic April 2, 2026 Specifications that move through time