Confidential engagement
Quint · AI
Portfolio
Selected work with client teams on distributed systems and blockchain protocols.
Workshop on efficient use of TLA+ tools
TLC · Apalache · TLAPS · AI
Grant on Hardened Testing of TLA+ Model Checkers
Specification and formal verification of the Aztec Governance Protocol
Formal specification; invariants checked; audit report.
Governance · Solidity · Quint · Apalache
Confidential engagement
Quint
Verifying ChonkyBFT: the consensus protocol of ZKsync
Executable spec; inductive invariants; research report.
Consensus · Quint · Model checking
Model checking of the 3SF Protocol
Accountability of 3SF; TLA+ spec & model checking; research report.
3SF · TLA+ · Apalache
Specification and model-checking of the ZKsync Governance Protocol
Quint specification; invariants; issue reproduction.
Governance · Upgrades · Quint · Apalache
Solarkraft: a runtime monitoring tool for Stellar
Open-source runtime monitor; adopted for contract checks.
Runtime monitoring · Soroban · Tooling
Selected clients
- Asymmetric Research
- Canonical Ltd.
- TLA+ Foundation
- Aztec Labs
- Matter Labs
- Ethereum Foundation
- Stellar Community Fund