Show HN: A Lean 4 port of libexpat's XML 1.0 parsing semantics

Category: library

Tags: lean4, xml-parser, formally-verified, parser, c-abi

Score: 6.3/10 (Innovation: 6, Technical: 8, Documentation: 7, Utility: 4)

lexpat is a Lean 4 reimplementation of libexpat's XML 1.0 parsing semantics, emphasizing safety for untrusted input via a total, resumable parser with machine-checked proofs and a bounded C ABI. Its technical depth (streaming, proof verification, differential testing) is impressive, but the niche combination of Lean and XML parsing limits practical adoption.

Target audience: security researchers, formal verification enthusiasts, systems programmers

Repository: https://github.com/scidonia/lexpat · Python · Apache-2.0

View on Hacker News