Verified efficient parsing for binary data formats

EverParse is a framework for generating verified secure parsers and formatters from domain-specific format specification languages.

The framework contains three components:

LowParse: At the core of EverParse is LowParse, a verified library of parsing and formatting combinators programmed and verified in F*.

3D: A frontend for EverParse to enable specifying data formats in an style resembling type definitions in the C programming language. We have used it to generate message validation code for use within several low-level C programs.

QuackyDucky: A frontend for EverParse that accepts data formats in a style common to many RFCs. We have used it to generate message processing code for several networking protocols, including TLS and QUIC.


We produce public releases under the form of a Windows or Linux standalone binary (amd64) package and a platform-independent source package.

The latest release of EverParse can be found here.



EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats;
Tahina Ramananandro, Antoine Delignat-Lavaud, Cedric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko; In Proceedings of the 28th USENIX Security Symposium, 2019

Indices and tables