1. Overview🔗

L4YAML is a pure Lean 4 implementation of the YAML 1.2.2 specification (RFC 9512). No external parsing libraries, no C dependencies in the core, and no use of partial def — every function is provably terminating.

The project demonstrates that a production-quality parser for a complex real-world format can be built and formally verified in Lean 4, with practical performance and comprehensive test coverage.

1. 1.1. At a Glance
2. 1.2. Key Design Decisions