The Tendermint LightClient specification in TLA+ was written and verified by Igor Konnov and Josef Widder at Informal Systems in 2019-2020.