9 ms·
Looking around for examples. Google can't find anything non-trivial. Do you know of something I can look at?
by Animats 1y ago
Looking around for examples. Google can't find anything non-trivial. Do you know of something I can look at?
- MaxBarraclough 1y agoPerhaps 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...