经过
AWS 的 Zelkova 验证访问策略：一段权限配置是否允许某种访问，两条策略是否等价，一次变更是否把禁区打开。它属于亚马逊云科技自动推理组把形式化验证应用于云安全与合规的一条路径，与 Tiros、CBMC 等并列，服务客户也服务内部开发者。工程上真正改变行业的，不是又一个求解器论文。是规模。Zelkova 通过构建抽象、消除规范撰写，五年内从每天约一千次 SMT 求解器调用，增长到每天约十亿次。从千到十亿，六个数量级。这个数量级意味着：验证不再是发布前请专家做一次的活动，而是策略被写下、被评审、被部署时就会碰到的门。
决定这个数量级的，不是 SMT 理论上还能证明什么更强的性质。是工程师用不用得上：延迟能否被等，失败能否被理解，误报能否被处理，结果能否变成「这次合并不得通过」。用不上的证明强度等于零覆盖。用得上的有限检查，可以盖住真正被改到的那一截配置。云上的权限是横切的。一次 IAM 变更可以越过应用全部测试。把分析放在变更路径上，是把横切变更重新打开那本账。
它示范的第三条是分级可以被自动化咬住。不是所有策略都需要定理证明器里最强的那一类。需要的是：这一次变更所涉及的访问，是否仍在被允许的集合里。问小了，才能问得频繁。问得频繁，才盖得住每天都在改的那一层。把每一次云上配置都写成 seL4 式精化，做不到。把每一次配置都只交给人工审计，也做不到。Zelkova 走的是中间那条：有限性质、机器检查、变更门禁、规模覆盖。
剖析
定义上，Zelkova 定义的是权限语句的行为，不是云上全部托付。禁区是「这段策略不得授权某类访问」。能力是快速判断。禁区与能力在工具内部是对齐的。云上真正的托付——存款、病历、航路——仍在应用里。权限分析通过，应用仍可执行假使命。它关掉的是「我们相信这次 IAM 变更看起来没问题」。它没有关掉「应用想做的那件事是不是托付」。
对齐上，策略文本、求解器编码、判定结果、是否允许部署，被拉到同一条门禁上。这是对齐在云配置层的工业形态。编码会错，求解器会超时，等价性会在简化后失真。可用性包含如何失败：超时不得被当成通过。失败必须显式。把超时当绿灯，是红许可证在自动化里的形态。
达成上，每天十亿次分析，达成的是覆盖率，不是一次具体业务的使命。覆盖率有牙齿：没有分析，变更进不去。牙齿咬住的是权限语句。业务行动仍要另绑。把 SMT 次数当成可信性已经完成，是把对象层与保证层再次压成一句广告。
人的位置被门禁改写。立法进入策略语言与允许的访问类。划界进入「哪些变更必须过 Zelkova」。审判进入求解结果：通过、拒绝、超时。工程师仍在，但不再是唯一盯着百万行 JSON 的人。把人从最不擅长的穷举里撤下来，放到对性质的命名、对误报的裁决、对超时的拒绝上。这与 Therac 的操作员按 “P” 相反，与光大一人开发实盘不足十五日也相反。规模不是为了取代人。规模是为了不把审判交给偶然。
对方法的借鉴必须克制。可用性 > 证明强度，不是正确性不重要。是：再强的证明，若不能出现在这一次变更里，等于没有。seL4 示范精化可以成为开发。CompCert 示范工具链可以关掉一截假设。Zelkova 示范日常变更可以咬住一截有限性质。三例合起来仍不是学。它们是基础工作。基础工作要被翻译成定义·对齐·达成里可失败的步骤，而不是被翻译成「云厂商已经做完」。
