Igor Konnov's page
You can always reach me by writing a message on
igor
at konnov
.phd
or
igor.konnov
at gmail
.com
,
Mastodon,
X-Twitter.
[2024] I have started the blog Protocols Made Fun :bowtie:
[2024] I am an independent security and formal methods research scientist. Let me know, if you have projects that require following expertise:
Specification, simulation, and verification of distributed protocols, e.g., in TLA+ or Quint
Testing of distributed protocols, e.g., blockchains and smart contracts
Security audits, e.g., Solidity, CosmWasm, Cosmos
Started and managed by me:
Quint Executable specification language (2021-2023)
Apalache: Symbolic model checker for TLA+ and Quint (2016-2023)
ByMC: parameterized model checker for threshold-guarded fault-tolerant distributed algorithms
The project ICT-103 Apalache supported by the Vienna Science and Technology Fund
Lectures on Quint, TLA+, and Apalache at the VTSA’23 summer school. Lecture material (August 2023)
Short talk on Quint (June 2023)
Apalache: symbolic model checker for TLA+. Extended version of the talk at TLA+ tutorial, co-located with DISC 2021 (October 2021).
How TLA+ and Apalache Helped Us to Design the Tendermint Light Client. Interchain Conversations 2020 (December 2020).
Model-based testing with TLA+ and Apalache, with Andrey Kupriyanov. TLA+ Community Event 2020 (October 2020).
Type inference for TLA+ in Apalache, with Jure Kukovec. TLA+ Community Event 2020 (October 2020).
Formal Spec and Model Checking of the Tendermint Blockchain Synchronization Protocol 2nd Workshop on Formal Methods for Blockchains (July 2020).
Tutorial at DISCOTEC/FORTE 2020, pdfs + video
Tutorial at VMCAI Winter School 2020: pdf
Curriculum Vitae, February 2024