-
📫 How to reach me: my website
-
🚂 I am currently working on:
- 🧑🍳 redacted 6 Cooking new specification and testing tools (think of TLA+ and Quint). DM me to learn more
- 💙 maintaining and improving Apalache — symbolic model checker for TLA+ and Quint
- 🍨 playing with proving correctness of distributed algorithms in Lean
- 💸 web3 security contests
-
Recent past work:
- 🧪 Symbolic testing of TFTP, see the blog post
-
Ⓜ️ redacted 5 TLA+ spec of a consensus protocol - 🔥 protocol specification of Aztec Governance and verification with Quint and Apalache
-
redacted 3 consensus spec audit - Solidity protocol audit for Aztec Labs
- ❓redacted 1 for Matter Labs
- 🍪 specification and model checking of ChonkyBFT for Matter Labs
- 🍩 model checking of 3-slot finality for Ethereum
- 🌟 runtime verification of Soroban/Stellar smart contracts with Solarkraft
- 🍬 specification and model checking of ZKsync governance
- 🍭 improving usability of specification languages with Quint
- 🎠 improving Apalache for finding bugs in smart contracts, dApps, and Cosmos protocols
-
🔦 You can find how to reach me on my konnov.phd.
-
💡 You can ask me about Quint, TLA+, and protocol specification.
-
😄 Pronouns: he/him/his.