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

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

Igor Konnov, Principal Scientist at Informal Systems

As part of our effort on Verification-Driven Development at Informal, we have specified 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.

Find out more on the Event: 👉 https://conversations.cosmos.network/

Subscribe to the channel to learn more about Cosmos. Join the newsletter by visiting https://cosmos.network and hitting the subscribe button.