如果在一个计算机参与操控的重要系统——比如汽车或医疗设备——出了软件错误，那将是灾难性的，有着“不必要的风险”的程序会将人们的性命置于险境，琼恩·阿迪朗达克(June Andronick)这样说，她是澳大利亚国家信息技术研究中心(NICTA)的研究员。以最近发现的一个软件漏洞为例子，她解释说，“可以攻击内置音响系统来控制一辆汽车。”她正在尝试减少这类风险，具体做法是让操作系统最重要的地方——核心，或说内核——受到保护而不会崩溃。
　　当前受到研究者青睐，让软件更加可靠的方法是在时间允许的情况下，尽可能地在各种各样的条件下进行测试。阿迪朗达克的替代方案是采用被称为形式验证的技术，芯片制造商用其来检测集成电路的设计：他们在芯片的子系统上安装一个数学表达式，这个子系统用于防止芯片被所有可能的输入控制。直至今日，在大程序(例如操作系统)上应用形式验证都被认为是不切实际的，因为分析程序代码的表达式实在是太复杂了。但是在一个计算机与数学的杰作之中，阿迪朗达克与她的同事们在NICTA的格尔文·克莱恩实验室中，已经对组成了绝大多数操作系统内核的代码进行了正式验证，这些操作系统广泛用在智能手机、汽车与便携式医疗设备这类的电子设备之中。因为这些代码最终绕过系统其他部分的软件指令而到达硬件进行执行，对它们进行防护对于整个系统的可靠性有着重大影响。
　　“这项工作意义重大，”剑桥大学的计算机科学教授劳伦斯·鲍尔森(Lawrence Paulson)说。比起证明在系统内核中没有可能导致崩溃的缺陷，验证可以保证内核始终运行无误，每一个编程实现的功能都能执行。
　　以研发微型内核的方式，可以让这个方案更容易实现。微型内核尽可能代替内核之外的软件模块需要执行的命令——例如对输入、输出的处理，相应的，它们都比较小，在之前提到的案例中，微型内核有大约7500行C语言代码及600行汇编语言。“它们对于系统内核来说很小，但对于形式验证来说的确很大。”阿迪朗达克说。需要针对数以千行的C语言代码进行分析，这就需要研发新的软件与数学工具。系统内核在2月份发布，研究小组正在对更为流行的X86架构的芯片代码行进行处理。
　　阿迪朗达克并不指望这项技术变成一个大型软件级别的东西，但她也不认为有必要这样。在关键的子系统中进行使用验证码，可以让开发者确保，在未经太多检查的程序中出现的错误不会影响到重要的硬件，例如那些与汽车音响接口的程序，这同样也能防止计算机在遇到问题时锁死。阿迪朗大克希望更多的软件生产商“在与安全和保卫紧密联系的地方”采用形式验证，她说：“我们已经验证这是可行的。”
　　——威廉·巴尔克利