Beyond selling tools:
tailored testing and verification for distributed systems where failure is expensive

Distributed protocols, bridges, consensus, governance: wherever standard tooling runs out and teams need something built to fit.

→ Book an intro call ↓ Engagements
At a glance
Experience
20+ years in academia & industry
Focus
distributed systems & blockchains
Methods
AI-assisted testing, model checking, simulation, fuzzing
Formal specs
TLA+, Quint, Lean
Targets
Rust, Golang, Solidity
§ 01 · Services
4 engagements
S-00

Consulting on TLA+ and Quint

Helping you with specification idioms, best practices, and tool understanding. Brought to you by the author of Apalache and Quint.

  • · Online calls and on-site meetings
1–4 hours
S-01

Specification review and strengthening

A structured audit of your existing specs, from English prose to formal specifications to find ambiguity, missing invariants, and underspecified behavior before they hit production. I'm equally comfortable working with implementation code, whether it's Rust, Go, or Solidity.

  • · Written report and review of your artifacts
  • · Safety invariants and liveness properties
  • · Simulation and model checking (optional)
1–2 weeks
S-02

AI-assisted specification & testing harnesses

Purpose-built harnesses that pair human-written protocol specifications with AI-driven conformance testing and counterexample generation. The specifications can be in TLA+, Quint, or *something else*

  • · Model-driven fuzzing of real implementations
  • · Fault injection
  • · Invariant checking
  • · CI-ready after handover
4–6 weeks
S-03

Protocol specifications & model checking

End-to-end specification and verification engagements, from pseudo-code to checked model to findings report, with the specs left in a state your team can maintain.

  • · Protocol-sized specifications
  • · Randomized symbolic execution, bounded model checking, invariant checking
  • · Handover to the team to avoid bit-rot
4–8 weeks
§ 02 · Engagements
6 selected

Paid work with client teams on production protocols.

§ 03 · Case studies
2 writeups

Methodology writeups on open systems: worked examples of how the tooling comes together.

#
Title
Scope
CS-01

AI-assisted conformance testing of TFTP

Human-written specification and LLM-assisted harness generation for five real TFTP implementations to surface protocol-level bugs traditional fuzzers miss.

Blogpost →
AI-assisted · TLA+ specification · Protocol testing · Python harness · Apalache
↗
CS-02

AI-assisted specification and conformance testing of ZooKeeper

LLM-driven specification and conformance testing of ZooKeeper.

AI-assisted · TLA+ specification · Distributed systems · Protocol testing · Python harness · Apalache
·
§ 04 · About

Researcher-practitioner at the intersection of formal methods and real distributed systems. Past: Informal Systems, Interchain Foundation, Inria, TU Wien. Principal investigator and developer of Apalache, a symbolic model checker for TLA+. Author of Quint. Based in Vienna, Austria, works across EU hours with the US, UK, EU.

→ Full research record
§ 05 · Contact
Working on something where a missed invariant costs real money?
→ Book an intro call
email
igor@konnov.phd
location
Vienna, Austria · EU
tz
Europe/Vienna
lead time
1–2 weeks