Baofa 的合约是依据参考程序的完整规格重写的，目标是可比对而不是可信赖。本页描述这套体系并坦率说明其状态，包括尚未完成的部分。
方法#
| 层 | 内容 |
|---|---|
| 规格表 | 参考实现的每个指令族一张表（数学、买入、卖出、发行、毕业、创作者收益、激励、错误、多跳、状态、事件；费用配置、查询、分成、社交与捐赠、回购；狂暴模式状态、交易、划转；中继捐赠、周期与兑换），每张表有编号规则与 EVM 强制的偏差，均经裁定并记录 |
| 差分测试 | 曲线与费用运算在参考实现的整数域上逐向量地与独立模型比对 |
| 单元与场景测试 | 每条函数路径、每个具名错误、每个事件结构 |
| 有状态不变量 | 托管恒等式（每条曲线的代币与计价资产）、钻石合约的零原生余额、费用账本守恒，在随机序列的每次调用后检查 |
| 分叉测试 | 在 BNB Smart Chain 分叉上对真实的 PancakeSwap v2 工厂与路由测试毕业 |
| 符号证明 | 用 Halmos 对受检运算与费用拆分在其完整操作数域上证明 |
| 静态分析 | Slither、Aderyn、为本代码库编写规则的 Semgrep、Solhint、forge lint 与 gitleaks，在门禁中运行，每次运行的结果记录在证据目录中并由工程团队分类 |
| 模拟主网演练 | 在私有链上以上线参数运行十万个随机场景，包含从已公开的发行平台与 AMM 事故中整理出的攻击类别，在专用服务器上执行 |
| 发布门禁 | 一个确定性脚本：构建、检查选择器、ABI、场景接口、惯用法规则、中继错误、事件结构与存储布局，运行测试并记录分析器；每一步把证据写入带日期的目录，运行以摘要结束 |
修复纪律#
每一个发现，无论内部还是外部，处理方式相同：先有一个修复前失败的概念验证，每个发现一次提交，概念验证作为回归测试保留，与参考实现的行为比对，任何偏离连同理由记录。超出所述根因的修复会在回应中说明。
当前证据#
交给外部审查方的包 baofa-rewrite-2026-11-04-a727bfe 包含上线合约的 75 个 Solidity 文件及其文档，从部署所用的同一提交切出。