A Million Lines of Proof About a Moving Target (Invited Talk).

In last ten years, we have been porting, maintaining, and evolving world's largest proof base, formal proof in Isabelle/HOL of seL4 microkernel. But actually, there is no such thing as the seL4 proof; there are a number of proofs (functional correctness, binary translation validation, integrity and confidentiality proofs, etc) about a number of instances of seL4 (depending on hardware platform it runs on, features it includes, extensions it supports). We will give an overview of current state of these proofs, and, importantly, challenges we face in keeping to maintain, evolve and extend them, and processes we have put in place to manage their dependence on evolving implementation.