@rzeta0 @sel4 "functional correctness" means the kernel always behaves to spec, no matter what you feed it.