Comment by twotwotwo

I think this rates as too obvious to say among anyone remotely close to this, but worth noting there is a lot of distance between an exploit and any real confusion.

Proofs aren't generally machine-read-only. An exploit of a proof system kernel doesn't necessarily look like normal proof code. Exploits can be fragile: 'safe' tweaks break them. If an exploit used maliciously is found, the person sneaking it through wouldn't exactly be thanked for it. And the window for exploits overall seems to be shrinking: Lean/nanoda are easier to secure than, say, Chrome.

If someone wanted to deliberately sow confusion (my career advice is not to do that!) they would probably have better luck with a subtly wrong formalization or an informal proof. If they have prover kernel bugs, they should report them and get free T-shirts.

Still, it's cool to see how they're hardening Lean.