Software

By language: Go (1) · Java (1) · Lean 4 (3) · OML (1) · Python (1)

Verified software in Lean 4

• L4YAML author Lean 4

  A YAML 1.2 parser in Lean 4 with machine-checked proofs.

  nasa-jpl/L4YAML

• PropertyKindCalculus author Lean 4

  Dybkær's kinds-of-property and quantity calculus, formalized in Lean 4 with PhysLib.

  nasa-jpl/PropertyKindCalculus

• doc-verification-bridge author Lean 4

  What theorems assume, prove, validate, and depend on? Bridging Verso docs and Lean proofs.

  NicolasRouquette/doc-verification-bridge

Formal metrology

• PropertyKindCalculus author Lean 4

  Dybkær's kinds-of-property and quantity calculus, formalized in Lean 4 with PhysLib.

  nasa-jpl/PropertyKindCalculus

• metrology-vocabularies author OML

  OML vocabularies for VIM3 / ISO 80000 metrology concepts.

  opencaesar/metrology-vocabularies

Model-based systems engineering

• openCAESAR co-lead Java

  Ontological Modeling Language and tooling for rigorous, agile MBSE at JPL.

  opencaesar/oml

• OpenSysML contributor Go

  Open SysML v2 tooling (Jupyter kernel, Airflow provider, OpenTelemetry bridge).

  Open-MBEE/OpenSysML

Compositional design and contracts

• Pacti co-author Python

  Assume-guarantee contracts for efficient compositional analysis and design.

  pacti-org/pacti

By language

Go

OpenSysML

Java

openCAESAR

Lean 4

L4YAML, PropertyKindCalculus, doc-verification-bridge

OML

metrology-vocabularies

Python

Pacti