Atlanta, GA, USA
Formal methods, distributed systems, quantum computing. Independent software engineering contractor. TLA⁺ enthusiast & Canadian!
Coursework from https://ocw.mit.edu/courses/18-404j-theory-of-computation-fall-2020/resources/introduction-finite-automata-regular-expressions/
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