I think that comparison is on point. A lot of the value here is in turning the spec into an attack surface, and that can surface failures that never show up in the clean reduction model, like serialization quirks or whether a KEM proof still holds after a tiny transcript tweak. What I found a bit surprising is how quickly the line between a real cryptanalytic break and a compliance bug gets blurry, because a universal forgery on paper can still hinge on one exact message format choice. That makes the output useful, but also harder to compare against NIST-style design work, where the failure modes are usually much more explicit.

And it rewards automated bug-farming shops, not the teams shipping safer primitives.