这是一个闭源的TEE OS，但其ATF组件已提交到upstream。
实现安全功能需要硬件的高级抽象，通常由操作系统 (OS) 提供。由于安全功能的正确性取决于这些高级抽象的正确性，因此实现这些功能的操作系统应该没有可利用的漏洞。
ProvenRun 开发了 ProvenCore，这是一款经过正式验证的超安全 OS/TEE，可应对这一挑战。对于能够以经济高效的方式开发许多领域（汽车、铁路、航空、能源、工业、医疗等）的安全设计连接设备而言，这是一个重要的里程碑。ProvenCore 使用演绎形式方法来：
- 提供优质代码（尽可能接近零缺陷）
- 以高级 API 的形式提供正确的抽象级别
- 具有可以正式验证并最终以可承受的成本获得认证的安全属性。
ProvenCore 已获得通用标准 EAL7 认证，这是通用标准认证计划定义的最高级别。
ProvenRun 成立于 2009 年，率先采用形式化方法和安全评估技术，使复杂软件达到最高级别的安全设计。ProvenCore 是第一个也是唯一一个获得最高级别 (EAL7) 通用标准安全认证的操作系统。它是物联网安全的绝对最佳基础。航空航天和国防、汽车和半导体行业的 OEM 和一级供应商可以更快地开发和认证应用程序，预测未来的监管要求，并降低生命周期维护成本。ProvenRun 的安全技术通过引领大规模部署和提高安全行业标准，建立了对物联网的信任。
