-
📫 How to reach me: my website
-
🚂 I am currently working on:
- ✨ making wonders with Wunderspec (if you like TLA+ and Quint, have a look)
- 💙 maintaining and improving Apalache — symbolic model checker for TLA+, Quint, and Wunderspec
- 🍨 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.
{{ message }}
konnov
Follow
Pinned Loading
Something went wrong, please refresh the page to try again.
If the problem persists, check the GitHub status page or contact support.
If the problem persists, check the GitHub status page or contact support.