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.