There is some discussion of this topic on the Isabelle mailing list: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00061.... 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