One of the critical issues when developing blockchain infrastructure is how to perform testing of complicated scenarios, involving multiple distributed nodes, possibly connected to several heterogeneous blockchains. While traditional tests are good and necessary at the level of unit testing, it becomes prohibitively expensive for developers to create (and maintain!) multi-node, multi-blockchain tests.

To address these needs, we are developing “Model Based Testing” (MBT) methodology and tools around the TLA+ specification language and the Apalache model checker, allowing us to auto-generate tests for real implementations (eg. in Go or Rust) from an underlying TLA+ model.

As an appetizer for our method, consider the IBC token transfer test, which spans more than 100 lines of code to setup the 3 blockchains and perform simple token transfers between them. In contrast to this manual test, a model-based test is the following 5 lines of TLA+:

TestUnescrowTokens ==
  \E s \in DOMAIN history :
     /\ IsSource(history[s].packet)
     /\ history[s].handler = "OnRecvPacket"
     /\ history[s].error = FALSE

While not obvious from the first glance, these 5 lines generate the complex setup with 3 blockchains and token transfers between them, which is roughly equivalent to the manual test referred above. In fact, this simple TLA+ test allowed us to catch a real bug in the token transfer IBC application. For details on this particular case see our recent talk at Interchain Conversations 2020; for the details on general MBT methodology please watch the talk at TLA+ Community Event 2020.

Model based testing matured significantly in the last six months: it is now part of the Tendermint light client test suites (part of CI), both in Rust and Go implementations. Light client model-based tests are derived from the TLA+ model of the Tendermint Light Client. The tests themselves are simple TLA+ assertions that describe the desired shape of the Light Client execution - see LightTests.tla for some examples. Expressing test scenarios as TLA+ assertions allows capturing very complex scenarios with just a few lines of high level TLA+ logic. MBT contains also basic fuzzing functionalities which allows more complex test scenarios compared to the traditional fuzzing libraries, as corrupted data structures can be injected as part of the non-trivial scenarios defined with TLA+ assertions.

MBT has already proved itself by catching several bugs, both in the light client Rust implementation (#650, #637 and #579) and in the token transfer IBC application in Go, which we touched upon above. In coming months, we plan to further improve developer experience of MBT so that development and maintenance of MBT tests can be under responsibility of the corresponding development teams. There is a clear interest from core Cosmos development teams to further expand their test suites using MBT.

On the methodology and tooling side, our MBT plans for Q1/Q2 2021 include:

If you’re interested in Model Based Testing for your own system, get in touch!!

Start your career with Informal Systems
Start your career with Informal Systems

Explore career opportunities at our cooperatively owned and governed organization, with world-class expertise in distributed systems, formal verification, and open-source ecosystem.

Apply Now