Formalising NASA-STD-5001B

In this repo, I used Lean 4 to formalise structural analysis tests for aerospace hardware. This repo does two things: it formalises key parts of NASA-STD-5001B,[1] then lets you plug in an FEA simulator and formally verifies the correctness of that simulator's computation.

Repo: https://github.com/OliverP255/nasa5001b-lean

References
  1. NASA. (2022). NASA-STD-5001B w/ Change 3: Structural Design and Test Factors of Safety for Spaceflight Hardware. standards.nasa.gov ↩︎

Oliver Pryce

I'm doing research to make engineered physical systems formally verifiable.

My Research