Blog

Two Definitions, One Use: Building SSA in a Haskell Compiler

2026-07-27 • 14 min read

What Was Actually Hard: Finishing a Verified Compiler in Lean 4

2026-07-26 • 15 min read

The Verification Gap: Building a Proven-Correct Compiler in Lean 4

2024-07-25 • 3 min read