informalsystems / vdd

Verification-Driven Development
21 stars 0 forks source link

Josef/vddverification #6

Closed josef-widder closed 4 years ago

josef-widder commented 4 years ago

This PR includes a spec for the blockchain (which includes soundness invariants), the light client verification (in VDD style which references the blockchain properties), and a full node spec that just includes the functions that the light client can access via RPC.

Comments are welcome!

The failuredetector.md in this PR is here for historical reasons. Don't look at it. The one in the tendermint/spec repo is the canonical one.