Apalache
Ongoing maintenance under TLA+ Foundation & Linux Foundation
Symbolic model checking for TLA+ with SMT solvers.
Independent researcher & consultant
I help teams verify distributed protocols with formal models, proofs, and tests.
- Formal verification
- TLA+ · Lean · Quint
- Programming Languages
- Rust · Java/Scala · Python · TypeScript
Hardened Testing of TLA+ Model Checkers
R&D Grant by TLA+ Foundation
Testing TLC and Apalache through fuzzing, differential testing, and metamorphic testing.
Quint
Past research & development
Executable specifications. Language co-author, project lead, product owner.
Selected Projects
Aztec governance
Client work · Specification and formal verification
ZKsync / ChonkyBFT
Client work · Consensus protocol verification
ZooKeeper
Technical case study · Specification and conformance testing
Selected clients
- Asymmetric Research
- Canonical Ltd.
- TLA+ Foundation
- Aztec Labs
- Matter Labs
- Ethereum Foundation
- Stellar Community Fund