lite-client/Blockchain.tla explain fault model with respect to the spec

informalsystems / verification

Specifications of the protocols and the experiments on their verification

9 stars 2 forks source link

lite-client/Blockchain.tla explain fault model with respect to the spec #11

Open OStevan opened 4 years ago

OStevan commented 4 years ago

During discussion with @konnov and @ancazamfir we discussed interesting states in which a model can find itself which might seem counter-intuitive from the view-point of the full blockchain implementation and situations in real life. Mainly how the model can move into the faulty state and how it can move out as time passes by.

josef-widder commented 4 years ago

I am currently finishing an English spec for the blockchain. I will make a PR in the next days, perhaps some of the text in there could be used as explanation. I am also happy to participate in future discussions on that issue. The Tendermint failure model and its consequences are quite intricate, and we should make any effort to clarify things!

ebuchman commented 4 years ago

Move to tendermint-rs?