[seL4] Good C, bad C, verifiable C