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.
Borrowing from Lanier: the words on this site are meant to be read by people, not machines.
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.
More about me →- FRP in Lean: Stateful combinators, safety, and liveness May 3, 2026
- FRP in Lean: 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: Linear Temporal Logic April 2, 2026 Specifications that move through time
- Reactive Programming in Lean Part 2: Execution traces March 15, 2026 Recording and reasoning about the states our programs pass through