Re: What surprises me is...
If only. What I was trying to say politely is that JAC lacks the capacity to produce valid proofs. He therefore cannot be expected to do an adequate security review of anyone's code, let alone his own.
Tooling can deal with classes of errors. Methodology can deal with more classes of errors. Careful discipline can ensure that methodologies are adhered to. But the unknown unknowns remain.