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" < [email protected]> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel > >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
