综合与等价性

重新综合计算本身#

反例引导归纳综合（CEGIS）根据行为与反例寻找替代计算。在适用的纯标量区域中，候选表达式采用不同的布尔算术基与求值结构。这可以改变表达式图本身，而非仅装饰原有指令。

用反例改进下一候选#

候选将提交至区域转换验证。若验证器找到产生差异的输入，该见证会反馈给综合过程，下一候选必须考虑它。由此形成具有明确结果的搜索与证明循环，而非仅凭少量样例通过便接受公式。

仅接受已证明等价的区域改写#

验证器区分 PROVED、COUNTEREXAMPLE_FOUND、OUT_OF_SCOPE 与 UNKNOWN_BUDGET_EXCEEDED，仅 PROVED 代表接受。求解预算耗尽不会被当作成功，超出支持语义模型的区域也不能套用其他范围的证明。

证明具有精确契约#

区域模型在声明的入口前提与栈帧义务下，比较精确的 32/64 位结果及陷阱行为。有符号位宽、溢出和除零都属于契约。回归场景覆盖缺失前提、陷阱通道差异、无结论求解及证明缓存行为。

这只证明已接受区域改写在限定范围内的正确性，并不证明整个应用无缺陷，也不证明受保护程序无法被逆向分析。应用验证与安全模型仍是独立职责。