L4YAML

 L4YAML: A Verified YAML 1.2.2 Parser in Lean 4🔗

Nicolas F. Rouquette

L4YAML 0.5.2 is a fully verified YAML 1.2.2 parser written in pure Lean 4. It delivers 4,807 machine-checked theorems across 131 proof modules, zero axioms, zero sorry, and zero partial def — while passing 100% of the YAML 1.2.2 specification examples and 100% of the applicable yaml-test-suite test IDs (225/225).

This manual documents the project's architecture, verification strategy, security model, and FFI bindings for C, Python, and Rust.

Conformance vs other YAML processors on the yaml-test-suite: see the YAML Test Matrix.

A PDF version of this manual is available for download: L4YAML.pdf.

Contents

  1. 1. Overview
  2. 2. Architecture
  3. 3. Verification
  4. 4. Security
  5. 5. FFI Bindings
  6. 6. Building
  7. 7. Testing
  8. 8. Test Results
  9. Index