3.1.1. Layer 1: Machine-Checked Proofs🔗

The core layer consists of 2,770 Lean 4 theorems across 63 proof modules (63,684 lines). These proofs are checked by the Lean kernel — the small trusted core of the system — and establish properties including:

• Soundness — every token stream produced by the scanner corresponds to a valid YAML grammar derivation

• Completeness — every valid YAML input is accepted (not rejected with an error)

• Progress — the scanner's input offset strictly increases on every step, guaranteeing termination

• Well-formedness preservation — internal invariants (indentation stack consistency, flow level balance, simple key lifecycle) are maintained across all scanner operations

• Pipeline composition — scanner and parser compose correctly to deliver end-to-end guarantees

3.1.2. Layer 2: Compile-Time Guards🔗

2,124 #guard statements are evaluated by the Lean kernel at build time. These are not runtime tests — they are kernel-evaluated assertions that must hold for the project to compile. A failing #guard is a build error, not a test failure.

Guards are used extensively for:

• Concrete scanner behavior on specific inputs

• Round-trip properties (parse → emit → parse = original)

• Token stream structure for specification examples

• Character predicate boundary conditions

3.1.3. Layer 3: Runtime Tests🔗

1,041 runtime tests across 19 suites provide additional coverage:

• Specification examples — all 132/132 YAML 1.2.2 examples

• yaml-test-suite — 225/225 applicable test IDs (354/406 total; 52 YAML 1.1/1.3 tests are correctly skipped)

• Property tests — randomized input generation for edge cases

• Mutation tests — systematic input perturbation

• Adversarial tests — handcrafted inputs targeting parser limits

• Round-trip tests — parse → dump → parse cycle validation