Writing

Notes from working with programming languages, proofs, and systems. Tutorials to work through, references to return to, and things I’m learning along the way.

Ongoing series · Lean 4

Lean from the Inside

Learning how Lean works, from dependent types to the kernel. Deep dives and small experiments, with code checked by Lean.

Explore the series →

Start with the foundations

Type theory → Elaboration → Tactics

View every series entry

Articles & guides

Standalone writing, newest first.

Reading Tamarin Prover Output: A Visual Tutorial
2026-04-29

Read proof trees, trace protocol attacks, and make sense of Tamarin’s dependency graphs.

Formal Methods Tutorial Security
Formalizing Program Analysis in Lean 4
2025-04-03

Build a verified program analysis with abstract interpretation and machine-checked proofs.

Formal Methods Programming
Datalog for Program Analysis
2024-06-13 · Updated 2026-06-26

Explore rules, relations, and fixpoints through an interactive program analysis example.

Programming Tutorial
Coq Cheatsheet: Tools and Tactics for Goal Solving
2023-12-19 · Updated 2026-06-26

A practical, interactive reference to everyday proof tactics, with worked examples.

Formal Methods Reference
Rendering LaTeX in Hakyll
2023-11-14 · Updated 2026-06-26

Add mathematical notation and theorem-style environments to a Hakyll site.

Web Development Tutorial