Microkernel that has been formally proven

[Chuck Petras]

The web page states that muen is the "first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level."

Are there any academic papers or 3rd party verification test plans/reports demonstrating this claim?

I've read the muen_report.pdf.

Any pointers will be appreciated.

Chuck

[Adrian-Ken Rueegsegger]

Hello Chuck,

Welcome to the list!

On 9/14/19 12:22 AM, Chuck Petras wrote:
> The web page states that muen is the "first Open Source microkernel that
> has been formally proven to contain no runtime errors at the source code
> level."
>
> Are there any academic papers or 3rd party verification test plans/reports
> demonstrating this claim?

The Muen master thesis and source code were released in August 2013. To
our knowledge, at that date there was no other Open Source microkernel
that applied formal verification to show absence of bug classes at the
source level. As described in the report (section 5.4.3), we used SPARK
2005 to show absence of runtime errors.

Since then work has progressed at a steady pace and many improvements
have been implemented, e.g. the source code has been upgraded to SPARK
2014, the verification of functional properties is ongoing and just
recently we made the code of the Tau0 static variant public [1].

Regards,
Adrian

[1] - https://git.codelabs.ch/?p=muen/tau0.git