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.