This seems to raise the question: is libdeflate fast? My overall impression of libdeflate is that it produces a similar output size to zstd but takes 40 times longer to do it. I realize these are different algorithms of course, but they aren't that different, both being in the Huffman line of the LZ family. So why is libdeflate considered a performance benchmark?

It’s probably just because a zstd implementation in Lean would be more difficult. The whole project depends on being able to have a correctness proof for the implementation, and implementing that for the DEFLATE algorithm is simpler.