To me, this bug is most similar to the Timsort bug back in 2015 [1].

Timsort is an ingenious hybrid sorting algorithm originated from CPython and many implementations including OpenJDK adopted it mostly via a source-by-source translation. Timsort particularly maintains a stack of sorted runs, and due to the construction there is a small enough finite limit in the maximum possible stack size. However the original CPython implementation didn't exactly match what was proven, so there were rare cases where stack overflow could happen. So this was a serious security bug in CPython, but wasn't in OpenJDK because Java instead threw an exception in that case.

Similarly, this WebP bug occurred because the largest table size was formally proven but it didn't match what was fed to the source code. This kind of bugs is not only hard to verify but also hard to review, because of course there is a proof and the source code seems to match the proof, so it should be okay! This bug suggests strong needs for approachable formal verification, including the use of memory-safe languages (type systems can be regarded as a weak form of formal verification), not human reviews.

[1] http://envisage-project.eu/wp-content/uploads/2015/02/sortin...

Specifically, since performance is crucial for this type of work, it should be written in WUFFS. WUFFS doesn't emit bounds checks (as Java does and as Rust would where it's unclear why something should be in bounds at runtime) it just rejects programs where it can't see why the indexes are in-bounds.

https://github.com/google/wuffs

You can explicitly write the same checks and meet this requirement, but chances are since you believe you're producing a high performance piece of software which doesn't need checks you'll instead be pulled up by the fact the WUFFS tooling won't accept your code and discover you got it wrong.

This is weaker than full blown formal verification, but not for the purpose we care about in program safety, thus a big improvement on humans writing LGTM.