本文是 Gilles Barthe 撰写的一篇关于安全形式化的章节，聚焦于证明助手（proof assistants）在安全领域中的应用。证明助手是一类交互式定理证明工具，如 Coq、Isabelle/HOL 等，能够对设计和实现进行严格的形式化验证，确保其满足预期的安全属性。本文系统地阐述了证明助手在四个关键安全方向上的应用：系统安全（如操作系统内核、微内核的隔离性与内存保护）、语言安全（如类型系统、信息流控制、内存安全）、安全编译（如编译器的语义保持、安全相关的编译优化与保护机制）以及密码学（如加密算法正确性、协议安全属性的形式化证明）。作者强调，除了验证功能之外，证明助手的一个重要动机是支持认证流程，即通过机器可检查的证明为安全关键系统提供高保证的认证依据。文章内容横跨计算机逻辑（cs.LO）和编程语言（cs.PL）两个领域，为安全研究者、开发者和认证机构提供了形式化安全验证的宏观视角和方法论框架。读者可以借此了解如何将严格的数学证明融入安全工程实践，以应对日益复杂的安全需求。