[jpgoldberg]

Interestingly Microsoft presented EverParse designed to produce verified parsers for these sorts of data formats at USENIX Security 2019. https://www.usenix.org/conference/usenixsecurity19/presentat...

But it's only for parsing the data. What gets down with it after parsing can still be buggy.