News & Publications

Interchain Conversations II: How TLA+ and Apalache Helped Us to Design the Tendermint Light Client

Igor Konnov, Principal Scientist at Informal talks about our Verification-Driven Development approach at Informal and our work to specify the Tendermint Light Client in English and TLA+. We show how TLA+ and Apalache helped us in understanding the protocol better. Importantly, the TLA+ specification and the model checking efforts enable model-based testing of the protocol implementations.

CSCON[0] Ethan Buchman - Free as in Banking

CEO of Informal Systems and co-founder of Cosmos, Ethan Buchman, talks about the history of central banking and the lessons the cryptocurrency and blockchain community can draw from a long history of centralized finance.

Model-Based Testing with TLA+ and Apalache

The TLA+ community hosted a virtual event to bring together practitioners and researchers to discuss the latest developments in TL+. Andrey Kuprianov, Research Engineer at Informal, and Igor Konnov, Principal Scientist, presented on Apalache - a symbolic model checker for TLA+. Check out the presentation, paper, and slides here.


Igor Konnov, Principal Scientist at Informal Systems, is the co-chair of CONCUR 2020, during QONFEST, a leading conference for formal verification enthusiasts.

RustConf 2020

Informal is a Gold Sponsor for this year’s RustConf2020. We are big fans of Rust, and have ongoing Rust projects including the Tendermint protocol and the InterBlockchain Communication (IBC) Protocol.

Informal Newsletter #2

This marks Informal System’s second newsletter where we share updates with the community on what we’ve been up to over the past few months. We discuss what we are working on, including the tools we are developing for formal verification, and their use on Cosmos protocols and software. Enjoy!


DISCOTEC is an academic conference on Distributed Computing Techniques. Principal Scientist, Igor Konnov, gave a tutorial on the Byzantine Model Checker.

Consensus 2020

Informal CEO, Ethan Buchman, presented a technical progress update and roadmap for Cosmos and an update on InterChain Foundation treasury management.

Informal Newsletter #1

Hello World! This is Informal’s inaugural newsletter. In this update, we share what we’re working on, including the specification of Cosmos protocols in TLA+ and implementing them in Rust. Check out what’s in store for the team, what we’re reading, and more!

Online Payments by Merely Broadcasting Messages

Daniel Collins, Rachid Guerraoui, Jovan Komatovic, Matteo Monti, Athanasios Xygkis, Matej Pavlovic, Petr Kuznetsov, Yvonne-Anne Pig- nolet, Dragos-Adrian Seredinschi, and Andrei Tonkikh. “Online Payments by Merely Broadcasting Messages,” in DSN, 2020. Source here

Verification of Randomized Consensus Algorithms

Nathalie Bertrand, Igor Konnov, Marijana Lazi ́c, and Josef Widder. “Verification of randomized consensus algorithms under round-rigid adver- saries,” Invited Submission to International Journal on Software Tools for Technology Transfer. Source here.

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol

Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them. By: Sean Braithwaite, Igor Konnov, Ilina Stoilkovska, Anca Zamfir, Ethan Buchman, Zarko Milosevic, and Josef Widder.