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

Yeah, this is really cool. I'm now deep in the rabbit hole of FSE encoding and ANS & tANS. The last time I poked my head in here, range encoding and arithmetic encoding were the state of the art for fractional entropy representations, but they both sucked. This is a million times better and so simple that I feel like I should have invented it myself.