search

EntEthAlliance / enhanced-bft

a workspace for developing improvements to BFT consensus
Other
8 stars 3 forks source link

Formal proofs requirement #54

Open drequinox opened 4 years ago

drequinox commented 4 years ago

Currently, in the requirements it is stated "MUST have a formal proof of correctness that we can show to regulators;" It is not clear that what is the full scope of this formal proof. Are we looking at Formal spec and a model with automated checking or more traditional mathematical approach?

shapeshed commented 4 years ago

This requirement seems to be very specific to Financial Markets use cases. EEA clients could be used in environments where there is no regulator. Whilst I think this is a good requirement I feel MUST is too strong.

kubasiemion commented 4 years ago

I also think this is too strong - the formal proofs start from assumptions and deal with idealizations. Very often it is side-channel issues (=from outside of the theoretical model) that spoil the show.