by nickvec 3 days ago
Yeah, extremely misleading title even if it is technically true semantically. The phrasing gives the impression that a bug was found in `lean-zip` as part of the proof boundary when it was part of the unverified archive-handling code.
The archive-handling code was in lean-zip, it just seems the verifiers forgot to write proofs for it (still a bug).
Thats not the main finding of the article however. The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded.
And it took them several thousand words to explain what you just said in a sentence.
Definitely one of my biggest pet peeves with articles / blog posts. There is so much fluff. Just get to the point!