¶Wuffs
Wrangling Untrusted File Formats Safely
A restricted language, with heavy annotations of facts and proofs, that compiles down to safe C. Intended for parsing binary file formats.
This page is also available via Gemini at gemini://dcreager.net/file-formats/wuffs.gmi