Atlanta, GA, USA


Formal methods, distributed systems, quantum computing. Independent software engineering contractor. TLA⁺ enthusiast & Canadian!


A tree-sitter grammar for TLA⁺ and PlusCal


An industrial-strength TLA⁺ parser, written in Rust


Rewrites TLA⁺ specs to use Unicode symbols instead of ASCII, and vice-versa


Check two firewalls for logical equivalence using Z3


A Z3-based analysis engine for Teleport RBAC rules