Ironclad is a real time, UNIX-like OS kernel built using SPARK and Ada for formal verification. This makes it highly robust and reliable for general purpose and embedded use case. It offers a familiar POSIX compatible interface, supports true simultaneous preemptive multitasking, and includes features like Mandatory Access Control (MAC) and hard real time scheduling. It comes with 100% free software. https://ironclad-os.org/
Ironclad

Ironclad is a free software formally verified kernel written in SPARK/Ada

@nixCraft I’m familiar with Ada and enjoyed tinkering with it in the past (I got curious because it looked a lot like Pascal/Delphi, which I know relatively well) but I never heard about SPARK.
@fuchsiii @nixCraft granted this really could be a gamechanger where it truly counts and where clock-accurate instruction execution is considered the bare minimum for acceptance...
Kevin Karhan :verified: (@[email protected])

@[email protected] this makes total sense for #CriticalInfrastructure control systems as well as #aerospace applications. - Which is good because there needs to be more competition to the likes of #VxWorks! #RTOS #Realtime #OS #OperatingSystem #FLOSS #Irobclad #IroncladOS

Infosec.Space