Andrew Helwer
A supposedly worthwhile contract I'll never do again
The current state of TLA⁺ development
TLA⁺ is more than a DSL for breadth-first search
TLA⁺ Unicode support
Wrangling monotonic systems in TLA⁺
FOSS I Love
Inlining SVGs for Dark Mode
Using TLA⁺ at Work
Pseudocode Showdown
Google Groups has been left to die
Can sanitizers find the two bugs I wrote in C++?
Two C++ bugs I wrote
Writing a TLA⁺ tree-sitter grammar
What's the difference between a computer and a rock?
The Missing Prelude to The Little Typer's Trickiest Chapter
Regexes in the Z3 Theorem Prover
Two pictures of quantum computation
How do you reason about a probabilistic distributed system?
Meditation
Taking my home work setup seriously
Doing a math assignment with the Lean theorem prover
Simulating physical reality with a quantum computer
Walking the faster-than-light tightrope
Checking Firewall Equivalence with Z3
Formal Verification, Casually Explained