Evidence-enabled verification for the Linux kernel