L4YAML

 L4YAML: A Verified YAML 1.2.2 Parser in Lean 4🔗

Nicolas F. Rouquette

L4YAML is a fully verified YAML 1.2.2 parser written in pure Lean 4. It delivers 2,770 machine-checked theorems across 63 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.

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