019 · 编译器被证明正确，错误还藏在哪里？ACDC 以 Axon 为对象，分别测试已验证核心、可信检查、未验证文本接口与机器语义；实验说明形式证明能封闭一部分错误，却不能替代对规格、信任边界和拒绝行为的测试。