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
NASA. (2022). NASA-STD-5001B w/ Change 3: Structural Design and Test Factors of Safety for Spaceflight Hardware. standards.nasa.gov ↩︎