Software — free catalog

lean4-yaml

A NASA software catalog entry available for reuse or request.

Find it in the NASA software catalog Open project or source

About this technology

Overview

Current YAML parsers are written in languages that do not provide good support for rigorous formal verification (e.g. Python, C, Perl). Formally verifying architecture specifications written in YAML files. Such files are organized according to an implicit YAML schema that, currently, is not specified because the YAML tools available do not support YAML 1.2.2 schemas.This lean-yaml library fills that gap, developed using Claude Code for VS Code with AWS Bedrock Claude Opus 4.6, courtesy of JPL's CAE Bedrock pilot. It provides:- **Production-ready YAML 1.2.2 parsing** - Complete syntax support with 98% test coverage- **Type-safe schema system** - `FromYaml`/`ToYaml` type classes for mapping YAML to Lean types- **Custom struct support** - Easy integration with user-defined architecture typesThis enables the development of **verifiably correct architecture management tools** in Lean4, where architectural compliance verification can be proven correct rather than merely tested.