[tialaramex]

Hi Nigel, Thanks for interjecting (and of course Thanks for WUFFS). I'm glad to hear that WebP is "on the Roadmap" but I think this sort of work ought to have been considered by vendors as a must-have, high priority project, rather than being sort of vaguely welcomed sideshow that's not on their critical path.

Yes, I actually think that the choice to unequivocally prove safety rather than to attempt to prove that you implemented something specific (but with the risk that our specification is wrong), is almost invariably the right choice for this problem space. It would not have been appropriate for the TLS 1.3 protocol (which has a machine proof that it satisfies our intended criteria stated in the RFC, modulo the Selfie attack and assuming our cryptographic primitives all do what they said they do), but it's exactly the right thing for say a DOCX parser, or ZIP parser, or a JPEG compressor or similar for which WUFFS is the right choice.