Research

Independent research on specification and verification of distributed protocols, with a focus on TLA⁺, Quint, Apalache, and the systems that need them.

Talks & lectures Curriculum vitae

Speaking at a conference, 2023

Research & open-source projects

Apalache

Symbolic model checker for TLA⁺ and Quint. Ongoing maintenance.

Project notes →

2016–present active

Hardened Testing of TLA⁺ Model Checkers

Testing TLC and Apalache through fuzzing, differential testing, and regression tests. Supported by the TLA⁺ Foundation.

Project repository →

Current active

Quint

Executable specification language.

Another look at the logic of TLA⁺ →

2021–2023 past

ByMC

Parameterized model checker for threshold-guarded fault-tolerant distributed algorithms.

Github repo →

2011-2018 past

Roles

2024–present: Independent security & formal methods researcher
2020–2023: Principal Research Scientist · Informal Systems
2019: Senior Research Scientist · Interchain Foundation
2018–2019: Researcher · Inria Nancy — Veridis Team
2011–2018: Researcher and assistant professor · TU Wien — Forsyte
2003–2011: PhD student and researcher · Lomonosov Moscow State University

Publications

Full lists of publications and preprints:

PhD alumni

Dr.in Marijana Lazić
Dr. Thanh-Hai Tran
Dr. Jure Kukovec

Conference organisation

Co-Chair of CONCUR 2020 with Laura Kovács. More in the CV.