Accession Number:



Verified OS Interface Code Synthesis

Descriptive Note:

[Technical Report, Final Report]

Corporate Author:


Report Date:


Pagination or Media Count:



The outcome of the project is that they have solved some fundamental challenges, but more work is required to integrate these results into the larger proof framework of the seL4 microkernel to be directly usable in practice. Beyond the stated project goals, the solution approach required and enabled them to address a more fundamental challenge the integration of different interactive theorem proving systems without sacrificing correctness guarantees. While again more work needs to be done to fully complete this integration in a way that is usable for a larger audience, this result means that the strong binary verification automation tools from the HOL4 theorem prover, which were used for the verified ML compiler CakeML, can now also be used in the IsabelleHOL system that was used for the verified seL4 microkernel. This combination increases proof productivity and enables larger, more expressive systems to be verified in the future.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

[A, Approved For Public Release]