On: Google discloses three severe vulnerabilities in A...

[geofft]

What is the process for patching seL4? How does e.g. adding a parameter to an existing function affect the proof, and what's the process for proving additional predicates?

[microcolonel → geofft]

The proofs are publicly available, though I can imagine there would be significant... overhead involved in adding functions to the system.