Ironclad is a partially formally verified, hard real-time capable kernel written in SPARK and Ada. This talk will delve into why Ada was chosen for development, advantages of Ada compared with alternatives like C and Rust for the use case of low level development, and how these advantages are used inside Ironclad with the concrete example of driver development inside the kernel.

More information about Ironclad can be found on the project's website.