Improper parsing is one of the most frequent and dangerous causes of software security weaknesses. Many of those are due to binary data parsed by handwritten code in memory unsafe languages. In this talk, I present EverParse, a library and tool to automatically generate efficient, provably secure parsers in C. A showcase application of EverParse is its deployment in Microsoft Hyper-V, the virtualization technology underlying the Microsoft Azure cloud platform. Today, every network packet passing through Azure is first parsed by code generated by EverParse, ensuring that only well-formed packets are accepted, and all others are rejected. EverParse has also been used successfully for a variety of other applications, including TLS, QUIC, X.509, and ELF. I describe how EverParse helped us solve the challenges we encountered across these applications: 1/ how to come up with a formal specification for those data formats based on standards and existing code; 2/ how to generate formally verified parser code from such a format specification with least user proof effort; 3/ how to deploy and maintain such verified code into production. Based on our experience, I posit that formally verified binary data parsers are a sweet spot for software hardening in high-impact scenarios with least user effort. From there, I also survey some further challenges and opportunities, ranging from support for more data formats (ASN.1, CBOR, etc.) to AI-assisted format specification discovery.