望安科技形式化验证工具W-Cert面向形式化建模与验证，可以有效支持从安全要求、安全策略、安全功能规范到安全设计的形式化建模与验证，并提供CC评估所需的形式化证据。W-Cert可基于CC标准推荐使用的lsabelle定理证明器，提供安全性质所需的一阶高阶逻辑描述方法、安全策略模型和功能规范所需的抽象状态机统一建模。

W-Cert工具具备设计模型所需的State Monad模型描述语言，以及支持CC证据所需的一致性、符合性和安全性的逻辑推理系统。可极大降低开发人员对形式化验证技术和CC形式化要求的掌握，使其重点关注产品本身的模型和验证。