I'm not sure how I forgot to mention this project, especially considering how high quality it is: - https://www.muen.sk/ https://www.muen.sk/ Muen is implemen

I'm not sure how I forgot to mention this project, especially considering how high quality it is: - https://www.muen.sk/ https://www.muen.sk/ Muen is implemented in SPARK, and has been formally proven to contain no runtime errors, which is an incredible accomplishment.