Perhaps the Ironclad kernel [0] and SPARKNaCl? [1] Here's a search of the Alire packages for 'spark' [2]. Merely using SPARK doesn't mean full formal verifica

Perhaps the Ironclad kernel [0] and SPARKNaCl? [1] Here's a search of the Alire packages for 'spark' [2]. Merely using SPARK doesn't mean full formal verification of all correctness properties, as SPARK can be used at different 'assurance levels' from stone (no real formal verification but you restrict yourself to the SPARK subset of Ada) to platinum (full verification). [3] [0] https://ironclad-os.org/ https://ironclad-os.org/ [1] https://github.com/rod-chapman/SPARKNaCl https://github.com/rod-chapman/SPARKNaCl [2] https://alire.ada.dev/search/?q=spark https://alire.ada.dev/search/?q=spark [3] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...