@0xabad1dea @mario @shelldozer Yeah, although couldn't that be minimised a lot by running the checks on different kinds of hardware and underlying implementations? (Given portable enough code)

Also coming from a more "trusting trust" point-of-view, quite glad they note that proving Coq in Coq itself has quite few problems.