[shakna]

There was also Larch/Ada [0], which was a formally proved subset of Ada, developed for NASA [1].

[0] https://apps.dtic.mil/sti/tr/pdf/ADA249418.pdf

[1] https://ntrs.nasa.gov/citations/19960000030