Principal scientist at Informal Systems
You can always reach me by writing a message on
The meta-site of my academic sites, permanently under construction
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, December 2020