You can always reach me by writing a message on igor at konnov.phd or igor.konnov at gmail.com.

Open for incoming requests

Apalache

Symbolic model checker for TLA+

Protocol audits and research

Protocol audits and research for Web3

Model Checking Accountability in Ethereum

Exploring Automatic Model-Checking of the Ethereum specification

Quint

Alternative syntax for the logic of TLA+

Solarkraft

A runtime monitoring tool for Stellar Soroban, powered by TLA+ and Apalache