1风险驱动的验证计划
闭卷重建风险驱动的验证计划的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2规约评审与需求追踪
闭卷重建规约评审与需求追踪的对象、公式、算例、算法与失败边界。
3验证与测试的组合
闭卷重建验证与测试的组合的对象、公式、算例、算法与失败边界。
4安全协议与密码实现验证
闭卷重建安全协议与密码实现验证的对象、公式、算例、算法与失败边界。
5编译器、内核与硬件精化
闭卷重建编译器、内核与硬件精化的对象、公式、算例、算法与失败边界。
6标准、认证与独立复核
闭卷重建标准、认证与独立复核的对象、公式、算例、算法与失败边界。
7综合项目：从规约到可复现证据
闭卷重建综合项目：从规约到可复现证据的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：每条形式化性质要追到需求、危害和测试；需求变更反向标出受影响证明。；公式：traceability coverage=linked requirements/total。；算例：40条需求中36条有性质或测试链接，覆盖率90%。；边界：验证实现符合错误规约；孤儿性质无人解释业务意义。。
对象：验证投入按故障严重度、发生可能、暴露和可检测性分配，而非全项目同等级。；公式：priority=severity×likelihood×exposure/detectability。；算例：严重8、概率.2、暴露10、可检测2，优先级代理8。；边界：为易验证模块投入全部资源，关键接口只做单测。。
对象：协议验证关注认证、机密、重放与密钥状态；实现还需常数时间和内存安全。；公式：secrecy: attacker⊬secret。；算例：协议模型保密，但比较函数按首个不同字节提前返回，产生时间侧信道。；边界：Dolev-Yao模型证明直接等同真实密码安全。。
对象：证明覆盖模型内全称性质，测试/模糊测试覆盖模型差异、集成和性能；二者互补。；公式：assurance=proof_evidence∪runtime_evidence。；算例：核心算法证明数组不越界，集成测试发现序列化长度单位错误。；边界：验证后删除所有测试；测试通过后跳过关键证明。。
对象：安全关键认证需要可追踪工件、工具资格、独立评审和变更影响，而不只工具绿灯。；公式：evidence package=(spec,proof,test,trace,review,config)。；算例：六类证据缺独立review，包只完成5/6≈83.33%。；边界：供应商报告不可复现；配置变更未重认证。。
对象：端到端保证需连接源程序语义、编译器保持、内核隔离和硬件模型。；公式：Beh(binary)⊆Beh(source spec)。；算例：源代码无未定义行为且编译器已验证，才可传递源级性质；否则链断。；边界：只证明源码忽略编译器bug；含UB仍援引保持定理。。
对象：项目应交付可执行模型、实现、契约、证明、模型检查、代码测试、失败注入和局限报告。；公式：pass=spec∧semantics∧proof∧modelcheck∧tests∧replay。；算例：六项硬条件有一项失败，严格验收仍失败。；边界：只演示成功案例；把solver unknown隐藏为通过。。