3 ms·

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 th

by nickvec 6mo 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.

grg0 6mo ago
And it took them several thousand words to explain what you just said in a sentence.
- nickvec 6mo ago
  Definitely one of my biggest pet peeves with articles / blog posts. There is so much fluff. Just get to the point!
minimaltom 6mo ago
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.
- deleted 6mo ago
  [deleted]