It's beyond me why such foundational libraries don't have formal correctness proofs attached these days.

imo, partially because it's still not easy (in terms of code -> formal proof). With AI, I've been Lean-ifying a simpler (but non-trivial) algo. Pointing (current) AI at it only goes so far and in fact might go "too far" in certain cases, where a non-formalized argument would have sufficed. There's also "who watches the watcher" -- did it really prove what we're supposed to prove?

For something like these compression algos, though, I imagine it would be much easier since they already have actual proofs out there.