igor@konnov.phd konnov

Independent Researcher in Formal Verification and Security, with degrees and experience in academia and industry

Achievements

konnov /README.md

📫 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
- M️ redacted 5 TLA⁺ spec of a consensus protocol
- 🔥 protocol specification of Aztec Governance and verification with Quint and Apalache
- :shipit: redacted 3 consensus spec audit
- :shipit: 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.

apalache-mc/apalache apalache-mc/apalache Public

APALACHE: symbolic model checker for TLA+ and Quint

Scala 574 49
quint-co/quint quint-co/quint Public

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

TypeScript 1.5k 132
leanda leanda Public

Distributed algorithms in Lean 4

Lean 15
itf-py itf-py Public

Python library to parse and emit Apalache/Quint traces as JSON ITF

Python 4
freespek/ssf-mc freespek/ssf-mc Public

EF project Exploring Automatic Model-Checking of the Ethereum specification

TeX 8
aztec-governance-formal-verification-2025q3 aztec-governance-formal-verification-2025q3 Public

Quint specification of Aztec governance and formal verification

Bluespec 2