Dear all, The first of these terms has an... interesting history. In a nutshell, it's not always used appropriately. Clearly that's not going to be the case with SEL4, but what exactly is meant? Mixed critical is another term that I'm cautious over. It's not completely clear to me if the mixing refers to relaxed constraints for utilisation reasons or something else. (Correct me if I'm mistaken, but I don't think SEL4 implements FLASK, which would be the obvious way to provide differing constraints, relaxed constraints within the trusted computing model. It's totally the wrong level.) I have absolutely no doubt SEL4 will retain all the provable integrity ever claimed (by anyone involved), but this experimental-proto-main branch confuses me on what fundamentally changes. Jonathan Day