What is it about?
Ironclad is a partially formally verified, hard real-time capable kernel for general-purpose and embedded uses, written in SPARK and Ada. This paper delves into what the kernel is capable of, what makes it special, the future of the project, and what can be taken away for other projects.
Featured Image
Why is it important?
Delving on the internals of Ironclad can be useful for prospective developers looking into adding some of its characteristics to their own designs
Read the Original
This page is a summary of: Ironclad: A Formally Verified OS Kernel Written inSPARK/Ada, ACM SIGAda Ada Letters, May 2025, ACM (Association for Computing Machinery),
DOI: 10.1145/3742939.3742960.
You can read the full text:
Resources
Contributors
The following have contributed to this page
