Our vision to verify the security of large and complex systems is to: (i) design the system as a componentised, kernel-based system, with a minimal Trusted-Computing-Base, and (2) make use of the kernel’s access control mechanism to isolate trusted components from untrusted parts, allowing to concentrate the verification effort on the trusted components. In this talk I will explain our work in turning this vision into a real, formally verified system. We are considering a multi-level terminal system, and the formal verification of the absence of unauthorised information and data flows. This work includes the development of a framework to minimize the manual proof effort required for each system. It leverages existing proofs of access control and information flow at the kernel level, in our case seL4, to automatically decompose the proof and only require manual proofs for the trusted components. The end goal is to provide a repeatable process for the design and verification of low-cost, high-assurance systems.