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 https://app

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 https://apps.dtic.mil/sti/tr/pdf/ADA249418.pdf [1] https://ntrs.nasa.gov/citations/19960000030 https://ntrs.nasa.gov/citations/19960000030