We formally verified memory safety for inflate_table, a 266-line function in zlib where low-level memory operations depend on subtle algorithmic invariants. Starting without an existing C-to-Lean verification pipeline, we built one and produced a ~20,000-line Lean proof of memory safety and termination. LLMs generated most of the proof, while Lean checked every step.