Formal proofs requirement

[drequinox]

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]

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]

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.