search

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
4 stars 0 forks source link

Add invariant for checking accountable safety #34

Closed thpani closed 3 months ago

thpani commented 3 months ago

Add an invariant for checking accountable safety.

This definition only works with uniform voting power; we have to generalize it to weighted voting power in #33.