微软表示：“汇编语言（TAL）和霍尔逻辑可以确保低级代码中不会出现多种错误，我们使用汇编语言和霍尔逻辑来实现一个新操作系统Verve在安全性方面的高度自动化、静态验证。”
“我们的技术和工具能自动验证操作系统、运行时系统、驱动和应用程序中的每个汇编语言指令的安全性，实际上，它们会验证除了引导程序之外系统的每一部分的汇编语言指令的安全性。”也就是说，通过对每条汇编指令的自动验证微软可以确保整个操作系统的安全性。
微软Verve白皮书下载：
http://research.microsoft.com/pubs/122884/pldi117-yang.pdf
文/驱动之家