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.