Visible to the public Using the Cambridge ARM Model to Verify the Concrete Machine Code of seL4