Linked by Thom Holwerda on Wed 22nd Jan 2014 13:47 UTC, submitted by fran
OSNews, Generic OSes

The Muen Separation Kernel is the world's first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. It is developed in Switzerland by the Institute for Internet Technologies and Applications (ITA) at the University of Applied Sciences Rapperswil (HSR). Muen was designed specifically to meet the challenging requirements of high-assurance systems on the Intel x86/64 platform. To ensure Muen is suitable for highly critical systems and advanced national security platforms, HSR closely cooperates with the high-security specialist secunet Security Networks AG in Germany.

The webpage contains instructions for building the kernel yourself, for installing it in a virtual machine, and for running it on real hardware.

Thread beginning with comment 581354
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE: Brownie points...
by pgeorgi on Wed 22nd Jan 2014 15:19 UTC in reply to "Brownie points..."
Member since:

...for using Ada

The kernel is written in SPARK, so in addition to all the safety checks Ada does, the build system ensures at compile time that there won't be exceptions.

And the plan is to go beyond that and run proofs about domain specific runtime behaviour, too.

Disclosure: There are a number of commits in my name in there.

Reply Parent Score: 11

RE[2]: Brownie points...
by Sparky on Wed 22nd Jan 2014 23:01 in reply to "RE: Brownie points..."
Sparky Member since:

Great! I used SPARK Pro and GNAT Pro for about five years at a previous job. I was very impressed with the maturity and effectiveness of the tools and concepts. For us, it delivered what it promised. It took our team over a year to learn to use it well, but after that everything went pretty smoothly.

Reply Parent Score: 2