Tags

TLA⁺ is more than a DSL for breadth-first search TLA⁺ Unicode support Wrangling monotonic systems in TLA⁺ Using TLA⁺ at Work Pseudocode Showdown Writing a TLA⁺ tree-sitter grammar The Missing Prelude to The Little Typer's Trickiest Chapter Regexes in the Z3 Theorem Prover How do you reason about a probabilistic distributed system? Doing a math assignment with the Lean theorem prover Checking Firewall Equivalence with Z3 Formal Verification, Casually Explained

TLA⁺ is more than a DSL for breadth-first search TLA⁺ Unicode support Wrangling monotonic systems in TLA⁺ Using TLA⁺ at Work Pseudocode Showdown Writing a TLA⁺ tree-sitter grammar

Wrangling monotonic systems in TLA⁺ Using TLA⁺ at Work How do you reason about a probabilistic distributed system?

Two pictures of quantum computation Simulating physical reality with a quantum computer Walking the faster-than-light tightrope

What's the difference between a computer and a rock? Formal Verification, Casually Explained

Meditation Taking my home work setup seriously

Can sanitizers find the two bugs I wrote in C++? Two C++ bugs I wrote

Regexes in the Z3 Theorem Prover Checking Firewall Equivalence with Z3