OK so this article is sort of about formal proof automation, but it seems more practically about Zstandard, which I very much enjoyed reading.