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
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