mbrotli and mzstd are Rust implementations of Brotli and Zstandard whose developers are adding machine-checked proofs that selected functions follow RFC 7932 and RFC 8878. Differential testing against the C libraries, fuzzing, Miri and AddressSanitizer can show agreement with those libraries and help detect memory errors, but cannot establish standards compliance: both implementations may share a mistake. CVE-2026-111497 exposed that gap. The C Brotli decoder ignored a failed block switch, and mbrotli 0.5.16 likewise accepted streams the RFC declares invalid, though safe Rust prevented memory corruption. Version 0.5.17 fixed the deviation.
The proofs use Charon to extract Rust MIR and Aeneas to translate it into Lean 4; theorems then connect the translated functions to a hand-transcribed RFC specification. CI checks that translations stay synchronized with the Rust code. Early results cover mbrotli’s distance and length codes, last-distance ring and command packing, plus mzstd’s frame and block headers, sequence counts, code tables, repeat offsets and FSE states. They establish conformance, encoder-decoder round trips and, for covered inputs, absence of panics or overflow. These are substantial but partial proofs, not verified codecs: bit readers and writers, Huffman and FSE machinery, dictionaries, a Lean reference decoder and a proof that the Rust decoder refines it remain. The work also relies on assumptions about the translation tools and RFC transcription; byte-for-byte agreement with C and SIMD code remain matters for testing.
Summary generated by AI from the linked article. hn.today is not affiliated with Hacker News or Y Combinator.
GitHub’s opt-in public preview puts pull request merge readiness and next steps at the top of a compact Overview page. It also adds filters for unresolved conversations and your comments, plus newest-first comment sorting. (github.blog)
An amd64 system was upgraded from NetBSD 11.0 to 11.1 using sysupgrade, which downloaded the new system files and guided configuration merges. A certificate rehash check failed but was fixed with certctl, and pkgin repositories also needed updating for 11.1. (dwarmstrong.org)
Five unconventional programming books shaped the author’s thinking, covering assembly optimization, scientific computing, fractals, and programmer interviews. They stand out for showing programming languages applied to serious problems rather than toy examples. (prog21.dadgum.com)
Datastructures-JS is an open-source JavaScript project with TypeScript support. Its repositories include implementations of priority queues, search trees, linked lists, graphs, and sorting algorithms. (github.com)
Borland Turbo Pascal 7 streamlined Windows development with an integrated debugger, an accessible Pascal environment, and the Object Windows Library. The author used it to build medical imaging software and praises its affordability and polished tools, which Delphi never matched in impact. (kevinboone.me)
Discord’s new Rust-based Windows client loaded its friends list faster than the Electron app and used 290 MB of RAM with two accounts signed in. Discord says both apps were cold-started, highlighting the potential performance gains from replacing Electron. (windowslatest.com)
Today's best Hacker News stories, summarized and screenshotted, one email a day.