MathGraph.
Immutable public evidence

L4YAML parser acceptance — pinned source check

A source-pinned observation record over one exact L4YAML revision and one exact external suite. It preserves what ran, what matched, what differed, and what remains unknown.

Open record JSONVerification details

Version 1

Evidence resultWarranted — bounded
LifecycleCurrent

Historic snapshot
2026-10-10

Metadata updated 2026-10-10 · evidence unchanged

No affiliation or endorsement implied. This record is an independent check of public third-party code.

48/48Decoded cases matchedExact pinned YAML-suite source labels
31Expected acceptancesObserved acceptance matched source label
17Expected rejectionsObserved rejection matched source label
52/52Lean guards evaluated48 cases plus four executable controls
Verification boundary

One result. Several independent axes.

Passing a finite suite does not establish a universal theorem. Replaying named proofs does not certify natural-language intent. This record keeps those questions separate.

Source identity

Implemented

Git commits + blob receipts

L4YAML 62bf7077910e and YAML suite da267a5c4782 only.

Formal verification

Scoped replay

ORIGINAL_JPL_LEAN_PROOF_OBJECTS

Named executable factorization and scoped anchor-event lemmas only. Universal YAML correctness: UNKNOWN.

Finite execution

Pinned cases checked

LEAN_GUARDS_AND_COMPILED_TRYPARSE

48/48 decoded cases matched source labels; 4 additional controls; 52 total guards.

Statement fidelity

Unknown

No qualified translation service

Natural-language or source-intent correspondence was not independently certified.

Generalization

Unknown

No whole-language theorem

The observations do not establish parser correctness for YAML as a whole.

Current requalification

Not checked

Historic snapshot only

Newer L4YAML or YAML-suite revisions have not been requalified by this record. Machine status: NOT_CHECKED_AFTER_SNAPSHOT.

Immutable identity

Address the record, not a moving claim.

The content digest binds this exact publication object. It proves byte identity under the record's canonicalization rule—not the truth of claims outside its evidence boundary.

Record ID

mg-l4yaml-source-check-20261010

Content SHA-256

f0d092974d5d710fe9e17fb6759a894f2c28f2d3f5456439c071bd0a71c8d3cb

Schema: mathgraph.public-consequence-record.v1

Permanent URL: https://mathgraph.org/records/mg-l4yaml-source-check-20261010/v1/

Pinned sources

Every observation resolves to exact public code.

The JPL source pin is a merged feature-branch revision, not default main. Attribution does not imply JPL or NASA affiliation, approval, or endorsement.

L4YAML source repository ↗nasa-jpl/L4YAML@62bf7077910e888a0bc8adfc8e08a5f500ff3ca3YAML test suite ↗yaml/yaml-test-suite@da267a5c4782e7361e82889e76c0dc7df0e1e870
Branch at source pin
fix-a-grammar-completeness
Lean toolchain
leanprover/lean4:v4.34.0
Executable case scope
Pinned YAML-suite examples after specified source decoding
Qualified receipts

Two source executions, one publication gate.

Compiled parser and proof replay ↗Run 38018495536 · d49a17d2786e6d071af37d2aeba2f2dad7765b75Decoded source-native replay ↗Run 38020008793 · 988afbf9a6ec69488b63af5c7ff986fde26d673cStandalone publication qualification ↗Run 38021785401 · 13/13 assertions
Compiled receipt archive
b75581017d6620481c77e52b350e8bb8631d11747a92789f7887cde527807086
Decoded replay archive
61fc93815e3329c0490324f52897a94d3417044a5cf16a8e1e0f0109aa0e515e
Generated Lean source
a9a16f54c053e3c3c5a9f56486508a04ac84d9eb9e18106271daddac488d5b62
Negative lineage

The discrepancies stay in the record.

Qualification is not a cleanup operation. Historic misinterpretations and source-specific differences remain inspectable.

Known difference

Recursive anchor behavior

&x [*x]\n
Independent normative event model
ACCEPT
Pinned JPL parser
REJECT
Whole-input extraction theorem
UNKNOWN

This is a source-specific known discrepancy, not a novel bug claim and not a universal semantics finding.

Corrected lineage

26DV:0 input decoding

The first audit measured raw encoded whitespace and recorded one mismatch. The qualified V2 decoder applies the suite's visible-space convention; the native decoded guard passes. Both raw and decoded hashes remain recorded.

Decoder
yaml-suite-visible-space-only-v1
Raw source SHA-256
6a7b111962441781a368bdcb793ca5a4be450b65c2c82da48bca86f3d8944791
Decoded input SHA-256
b9ac5bb5babe113af697638577d77ee556dbc2d596bf05c5d31a8b402882976a
Unknowns

Not checked does not mean false—or true.

Explicitly outside this record

  • Universal correctness of the L4YAML parser or YAML as a language.
  • Natural-language, source-intent, or source-to-formalization fidelity.
  • Generalization beyond the 48 decoded source cases and four controls.
  • Requalification of any revision after the 2026-10-10 snapshot.
  • JPL, NASA, or YAML project endorsement of MathGraph or this result.
Durable resources

Inspect the original projection.

These committed assets are the byte-identical outputs of the qualified publisher. The OpenAPI document describes a localhost/preview resolver; it is not a promise of a live public endpoint.

Record JSON ↗Qualified immutable snapshotEvidence JSON ↗Source receipts and run identitiesOriginal generated evidence page ↗Publisher output preserved byte-for-byteScoped status SVG ↗48/48 pinned source casesResolver OpenAPI ↗Qualified preview contract; not publicly hostedRecord index JSON ↗Mutable catalogue · short-lived lifecycle statePresentation metadata JSON ↗Versioned sidecar · b415f4266f255b53a9878c0b1ded61d29a8e13dd00655a7992990648f566c7d6

Inspect this record’s canonical object projection → · All objects and declared relations