There is some discussion of this topic on the Isabelle mailing list:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00061.html

On Mar 20, 2016 1:44 AM, "Steve VanderLeest" <Steve.VanderLeest@dornerworks.com> wrote:
Since the formal verification of functional correctness of seL4 was performed using the Isabelle theorem prover, could someone tell me if Isabelle itself has been formally verified?  If so, could you suggest some good references to that work?

Regards,
Steve


Steven H. VanderLeest, Ph.D.
Chief Operating Officer
DornerWorks, Ltd.
3445 Lake Eastbrook
Grand Rapids, MI 49546
www.dornerworks.com


_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel