  In Tendermint blockchains, the proof-of-stake mechanism and the underlying
consensus algorithm entail a dynamic fault model that implies that the active
validators (nodes that sign blocks) may change over time, and a quorum of these
validators is assumed to be correct only for a limited period of time (called
trusting period). The changes of the validator set are under control of the
blockchain application, and are committed in every block. In order to check
what is the state of the blockchain application at some height h, one needs to
know the validator set at that height so that one can verify the corresponding
digital signatures and hashes. A naive way of determining the validator set for
height h requires one to: (i) download all blocks before h, (ii) verify blocks
by checking digital signatures and hashes and (iii) execute the corresponding
transactions so the changes in the validator sets are reproduced. This can
potentially be very slow and computationally and data intensive.
  In this paper we formalize the dynamic fault model imposed by Tendermint, and
describe a light client protocol that allows to check the state of the
blockchain application that, in realistic settings, reduces significantly the
amount of data needed to be downloaded, and the number of required
computationally expensive signature verification operations. In addition to
mathematical proofs, we have formalized the light client protocol in TLA+, and
checked safety and liveness with the APALACHE model checker.
