job(要完成的待办)
一次补全验证体系的既有缺口,并以 CNB 免费算力(CodeBuddy NPC 沙箱,每账号 1600 核时/月)作为发散侧底座。两条贯穿原则:
非确定生成 + 确定裁决 :LLM/CNB 只在生成侧(种子、变异体、不变量、蜕变关系、骨架、实现代码),一切判定锚点全机械(变异分数、运行结果、覆盖率、kernel 检查、hash 校验、交集/并集计算),判定语义零变化。
一致定义事实,分歧定义工作 :收敛的部分自动固化,分歧的部分自动路由(spec 歧义退回规划层、路线分歧存为策略菜单);fan-out 的预算由收敛带宽决定,与 token 无关。
A. 测试方法缺口闭环(对 quality 纲要差距报告的逐项落实)
变异测试实跑 + 定向变异体 :核查并落地 T-10 的 weekly 执行入口(stryker / go-mutesting,aws-tb 全仓);分数入 metrics 仪表盘 + 趋势下滑告警(趋势比绝对值重要);LLM(可跑在 CNB)生成定向变异体(瞄准高危分支/边界),候选经机械初筛(可编译、可被现有套件杀死率预演)后入池——分数核算与入池判定全机械,LLM 产物只是候选 。
属性测试不变量推断 + 交叉锚定链 :LLM 推断 aws-tb 纯函数区(判分、实例化、重组)不变量候选 → 机械过滤(可执行化为 fast-check/hypothesis 属性)→ 变异裁判 :不变量套件必须能杀死 T-10 变异体池中的成员,杀不死任何变异体的属性标记"平凡"并拒收——交叉锚定链(变异测试评属性测试,属性测试评代码)闭环。
模糊测试生成侧 + 深跑 :LLM 生成 schema 感知种子语料入 fuzz corpus;深跑(go test -fuzz 长轮)放 CNB 沙箱(低档位长跑,省 GitHub runner);崩溃样本机械去重(栈哈希)后 LLM 仅写分诊草稿 (人/机械裁决);锚点(唯一崩溃数、覆盖率增量)在 GitHub CI 汇总核算,不采信沙箱自报数字 。
蜕变测试领域盘点 :fan-out 盘点 aws-tb 领域自然蜕变关系(输入重排→结果集等价、重试→幂等、单元拆分→总量守恒、多语言实例化→同构等…)→ 结构化候选清单(关系 + 机械可验证实现方式)→ 人抽检 → 入 testing.yaml 触发式条款,并至少实现 3 条为常驻测试。
符号执行试点评估 :以 aws-tb 解析/实例化纯函数为试点目标,跑 pynguin/symbolic 工具链出运行时指标(路径覆盖、求解超时率、单位时间发现数);按三段式判据(是否要做/怎么做/设计质量有确定性评估)产出 adopt/reject 证据报告——adopt 则入 testing.yaml triggered 条款,reject 则按 X 条款格式登记并带 revisit_when ,两种结果都算验收通过。
SAST 误报分诊台账 :CodeQL/zizmor 告警处置结构化入账(告警指纹→处置:固修 PR / 豁免+ADR 引用 / 判误报+理由→入账 SHA);weekly 清点未处置告警并自动开 issue;误报率、豁免存量入 metrics——把"免费的 license、昂贵的分诊"这个持续成本显性化。
形式化验证:条件自动触发机制(修订 X-04) :X-04 从"无条件拒绝"修订为条件触发 (随本 IR 以 ADR 落实)。交付三件:
a. 结构化适用性 checklist (机器可读 YAML,C1 路径文件):正适用项(有清晰数学定义的算法核心 / 可建状态机的协议逻辑 / 密码原语 / 高风险且稳定的核心小块)与反适用项(无法脱离环境描述的胶水 / 无半形式化规范起点 / 演进中的契约 / 循环深度无界)+ 风险等级门槛 (业务输入,"这段代码错了要赔多少钱")——checklist 判断由弱模型(或纯脚本,凡卡元数据可机械判定的字段优先机械)按卡/spec 元数据执行,逐项判断与理由留痕入卡 ,可审计可重放;
b. 自动启动管线 :checklist 判"适用"即自动启动形式化作业(工具按栈选型并试点实测:算法核用 Dafny/crosshair 类、状态机用 TLA+ 类),kernel 检查为唯一锚点 ,证明通过/失败二值回写卡的验证面板;
c. 试点实跑 :aws-tb 挑 1–2 个正适用目标(判分算法核心、某状态机)真实跑通一次 kernel 检查全链(checklist 触发→作业→二值结果)。
卡/spec 模板新增 risk_level 字段(owner/业务显式给定;缺失 = fail-closed 按触发处理或退回补全 )。
B. spec 的 CI 与 spec 质量测量(不止 lint)
验收 DSL 编译器(承接 IR: 卡绑定测试与红队守门制度(LLM-as-a-Verifier 验证 + 意图兜底道闸) #263 ,不重复建设) :IR: 卡绑定测试与红队守门制度(LLM-as-a-Verifier 验证 + 意图兜底道闸) #263 已定 spec PR 必带 suite/ 与红队守门,但 suite 仍靠手写。本 IR 补机械层:定义受限验收 DSL (given/when/then + property + invariant);spec PR 中 DSL 书写的 AC 在合并时机械编译为 pytest 骨架 ,生成物携带 spec hash 溯源头;hash 校验入 gate——手改生成测试 = CI 红,想改判据必须回 spec 层 ;spec CI 关卡(schema 校验、DSL 可编译、blastRadius 申报路径存在性)入 specs/** 的 PR 检查链。存量 spec 不强制迁移,新增 spec 起强制。
spec 骨架 fan-out——把 spec 当程序跑,测"解读的方差" :每张进入 spec 阶段的卡,N=3–4 个独立骨架(路线陈述 + 接口签名草稿 + 测试草案 + 假设清单),CNB NPC 并行执行(一骨架一窗口)+ 至少 1 个异构自有 API 模型实例(防同源相关失败)。骨架是结构化制品,产出经纯机械计算:
分歧正交分解 (脚本执行):契约解读分歧(对"做什么"理解不同)= spec bug,spec 阶段必须修掉;路线分歧 = 健康方差,存为策略注入菜单 (实现阶段 fan-out 直接消费,骨架工作零浪费);
N 份测试草案的交集 = 高置信验收标准 (独立收敛到同一批用例 → 那批用例即契约本身,进 AC);并集 − 交集 = 模糊地图 (自动进红队攻击输入);
N 份假设清单去重后的并集 = spec 缺口的显式清单 (比从分歧反推更直接);
测量输出 :趋同度/分歧率作为 spec 质量指标入 metrics——高趋同 = 强置信信号;高分歧 = spec 歧义,自动退回规划层(分歧定义工作)。
C. 实现 fan-out、champion/oracle 生命周期与燃料管道(测"解的方差")
实现 fan-out + early-exit :实现阶段对通过决策矩阵 gating 的卡做 N 路并行实现(策略来自骨架阶段的路线谱系菜单 + 多样性注入):
决策矩阵(机器可判,入 policy) :高决策密度 × 高可判定 → 阻塞式 fan-out(黄金区);语义敏感 → 组合模式(merger 合成);低决策密度 → 单实例 + 机械门禁(打"免 fan-out"标签,趋同的历史卡自动获得);
Racing + early-exit :第一个通过全部 既有 gate 的实现立即合并(关键路径不等待,early-exit 不跳过任何 gate),其余转后台异步收尾;
后台评价 :后台实现对 champion 跑全量 gate + 性能 benchmark + 差分对拍;性能更优且对拍等价者走 improvement PR 替换现任 champion (替换必须过全 gate + oracle 对拍,双重裁决)。
champion/oracle 生命周期(对冲资产化) :
从不同路线簇 选亚军冻结为 reference oracle(跨簇 = 与 champion 错误模式去相关);
oracle 定位 = 测量仪器不是产品:住在 tests/ 里、不进生产、永不修 bug、只换代不修补 (换代 = 对着修正后契约重新 fan-out 重新冻结,免费算力下成本≈0);
权威边界:全体一致区 = 硬区(champion 与 oracle 分歧 = bug),缺口区 = 软区(分歧 = 契约审查信号);随修正案闭合缺口,硬区单调扩张;
champion 与 oracle 在硬区分歧 → 要么 bug 要么有意改行为——有意改行为必须先修契约 ("不修宪不得改行为"从纪律变机械执行);oracle 同时是语义 bisect 锚(生产 bug 时对语料库定位行为分岔点);
适用判据(机器可判):Tier A 表面 = 大输入空间 × 高改动频率 × 行为即产品;纯函数小输入空间 / 不动胶水不设 oracle。
fan-out 产物 → 红队与意图审查的燃料管道(有机打通) :fan-out 的副产物恰是红队与意图道闸(S6–S8)缺的结构化抓手,制度化直连:
骨架阶段产物 (条 9)→ 红队 round-2 的武装输入(分歧报告 + 模糊地图 + 假设清单并集——IR: 卡绑定测试与红队守门制度(LLM-as-a-Verifier 验证 + 意图兜底道闸) #263 已定"产出证据者先行"次序,本条落实管道);假设清单中涉及行为/边界的条目 = 意图道闸 S6–S8 的扫描候选,S8 blastRadius 比对纳入 fan-out 产物路径;
实现阶段产物 (条 10/11)→ 被淘汰实现与路线谱系成为红队差异攻击面 :对每条被淘汰路线,机械生成"champion 是否覆盖了被淘汰实现走过的边界/用例"类攻击查询,红队候选生成由 CNB 承接;后台对拍与 benchmark 分歧记录入红队证据源;
格式契约(管道即接口) :fan-out 产物统一结构化落盘(JSONL:类型 = 骨架分歧 / 假设 / 淘汰路线 / 对拍分歧,含卡 ID、spec hash、SHA 基准),红队与道闸的输入适配器只读该目录 ——产物即燃料,管道即接口;
趋同度突变(历史"免 fan-out"卡突然高分歧)作为弱信号入 metrics 观测面。
D. CNB 免费算力底座(临时措施、可删除层、发散侧专用)
独立仓 Cloudbird-Software/cnb-bridge(L2,public) :多账号调度器、派单协议、配额账本、账号 runbook、work-inbox 全部集中于此;核心治理对 CNB 的引用收敛为三接缝:GOVERNANCE.yaml EX-1 条目、org secrets(CNB_TOKEN_<alias>)、两个 workflow(cnb-dispatch / cnb-audit);REMOVAL.md 单页删除清单。
配额并入 cost 基础设施且作为配置存在 :charge/quota 定时快照 + build/logs 实耗对账 → append-only 账本 → 既有 metrics.py 仪表盘;余量 <20% 自动开 cost-infra issue;对账偏差 >10% 告警;账号与档位阈值全部是配置(automation-limits.yaml 新节 cnb:),加账号=改配置零代码 ;档位 light=1C(默认)/ std=2C / heavy=4C(须理由),8C 禁用,派单必填档位。
账号生命周期记录管理 :accounts.yaml(无明文 token)+ lifecycle.jsonl append-only 全程留痕 + runbook 每步带验收命令;验收 = 一个未参与开发的 AI 仅凭 runbook 独立完成新账号入职 。
work-inbox 强模型自起协议 :cnb-bridge/work-inbox.yaml 为强模型每小时自起的唯一工作发现入口——有 pending → 带 lease 认领 → 产出 → 写回释放;无 pending → 心跳行退出。lease 超时自动过期;清单 id 去重保证重复会话不重复派单。
fan-out 实现试点(自举) :试点卡从本 IR A 组选一张高可判定 卡,走通 C 组全链:骨架 fan-out(条 9)→ 策略菜单 → N=3 实现 fan-out → early-exit 合并 → 后台对拍与 benchmark → 亚军冻结为 oracle——一次试点把"spec 测量 → 实现 racing → oracle 资产化"整链打通。人类触点 = 1 次规划会话 + 1 次抽检。
周审计五项自动 :配额、活性(canary ≤60s)、延迟(派单→回复 p50/p95)、产物真实性(抽样 10% 机械核对重放)、政策监测(docs.cnb.cool 定价与 NPC 文档页 diff 自动告警);任一红 → CNB_DISABLED 置位建议。
E. 可脱离性演练(全自动)与 token 决策
演练全自动,零人工 :月度静态干跑(隔离不变式验证,自动出 issue);季度功能演练(自动置位 CNB_DISABLED → 发散链全量切 fallback 付费 API 跑一轮真实任务 → gate 全绿 → 自动复位 → 计时报告)。物理删除为一次性退休动作,不做演习 ;证明力边界如实入册(owner 裁决:接受证明力降低换零人工)。
token 决策入册(ADR) :现有高权限 token 保持不变;缓解条款:仅存 org secret、永不进 agent 上下文与 CNB 沙箱、泄漏应急 runbook 化。
触发场景
weekly 深层测试(变异/模糊)与发散型生成任务当前要么占用强模型会话,要么挤占 GitHub runner——瓶颈漂移定律指向"验证的生成侧"。
spec 的 AC 为散文,IR: 卡绑定测试与红队守门制度(LLM-as-a-Verifier 验证 + 意图兜底道闸) #263 强制 suite/ 存在但生成与溯源靠自觉;且spec 质量本身无测量仪器 ——歧义只能靠红队事后发现,成本高、发现晚。
实现是单实例串行:无 racing、无 early-exit;性能更优的替代实现无制度通道;重写项目无"行为等价性通行证"。
oracle 制度缺位:T-09 差分政策存在,但无 reference oracle 的创建/冻结/换代/权威边界管理——差分缺少长期对拍锚。
红队与意图道闸当前缺结构化抓手——攻击面靠 spec 文本与红队即兴探索;fan-out 副产物(骨架分歧/假设清单/淘汰路线/对拍分歧)恰是其天然燃料,缺管道则两相脱节。
X-04 对形式化是无条件拒绝,无判断机制——按纲要方法论,适用性判断应结构化为弱模型可执行的 checklist(一次性人类投入),触发应自动化。
强模型将以"每小时自起"运行,需要工作发现协议;owner 将带回数十个 CNB 账号,需要登记与生命周期管理。
CNB 政策/额度可能静默变化,当前无监测面。
quality 纲要对照报告(2026-08-23)确认缺口:符号执行零采用、变异/模糊政策与执行脱钩、蜕变仅两条示例、SAST 分诊无台账。
当前痛点的证据
T-10 变异测试:testing.yaml 声明 weekly placement,但已盘点 workflow 清单(.github 20 个、aws-tb 5 个、CI-Workflows 10 个)中无任何 mutation 执行入口 ——"声明存在、实跑未证"。T-04 fuzz 的 weekly(deep) 同样未见载体。
符号执行:全组织零采用痕迹。
蜕变测试:仅 L-03 两条示例(限 LLM 产品),领域盘点从未发生。
SAST 分诊:CodeQL 阻断已 enforced,但告警处置无台账——误报率与豁免存量不可见。
spec 的 CI:AC 为 YAML 散文,无 DSL、无编译器、无 hash 溯源;spec 阶段无骨架 fan-out——解读方差从未被测量过(红队 fan-out 测的是"攻击面共识",不是"解读分歧",仪器不同)。
实现侧:卡状态机与 gate 齐备,但实现恒为单实例;无 early-exit racing;无 champion/oracle 生命周期(aws-tb 的 tests/golden、tests/holdout 是枚举测试与隐藏测试,不是冻结的行为函数)。
红队/意图道闸的输入面:IR: 卡绑定测试与红队守门制度(LLM-as-a-Verifier 验证 + 意图兜底道闸) #263 的红队读 spec 原文 + 骨架(若存在),但骨架/淘汰实现/对拍分歧均无结构化产物目录,无输入适配器——燃料存在但没有管道。
X-04(formal_tla rejected)为无条件拒绝且 revisit 条件(写分布式协调组件)过窄——判分算法核心、状态机这类正适用目标当前没有任何进入通道;卡/spec 模板无 risk_level 字段。
dogfood 的 CNB 直连脚本无隔离、无记账、无健康检测;配额端点 2026-08-23 才确认;api_trigger 实测 400 未开放。
强模型 agent 无法无头启动(owner 陈述)——规划与执行时序耦合。
实测基线(zhuzhu-team/test,2026-08-23):issue NPC 26–28s 真实执行;runner.cpus 降配生效;build logs 可查;沙箱可克隆 GitHub 公开仓;NPC 无 logprobs(永不做判定)。
期望的可观察变化(验收时能在线上看到的事实)
A 组(测试缺口)
变异实跑 :aws-tb weekly mutation 分数入 dashboard;趋势告警注入测试触发一次;LLM 定向变异体入池记录(含机械初筛淘汰率)。运行时证据 :run 链接 + metrics JSON + 入池清单。
交叉锚定 :≥10 条不变量候选的机械过滤与变异裁判记录(含"平凡"拒收样本);存活属性常驻运行。运行时证据 :裁判日志(每条属性杀死的变异体清单)。
模糊生成侧 :种子语料入库与增长曲线;一次 CNB 深跑的崩溃/覆盖率 GitHub 侧核算;若有崩溃——去重指纹 + 分诊草稿。运行时证据 :corpus 历史 + 核算日志。
蜕变盘点 :≥15 条结构化候选 + 人抽检记录 + ≥3 条实现入册 testing.yaml。运行时证据 :清单 + 条款 diff + 运行记录。
符号执行试点 :adopt/reject 证据报告(含运行时指标);对应条款登记。运行时证据 :报告 + 指标数据 + diff。
SAST 台账 :ledger 建立并回填存量;weekly 未处置清点 issue;误报率入 dashboard。运行时证据 :ledger + issue + metrics。
形式化条件触发 :checklist 文件 + 一次真实自动触发全链记录 (弱模型判断日志逐项理由 → 形式化作业启动 → kernel 二值结果);一次判"不适用"的留痕记录;risk_level 字段入卡模板且缺失被 fail-closed 拦截的反向测试。运行时证据 :触发链日志 + X-04 修订 ADR diff。
B 组(spec 的 CI 与质量测量)
DSL 编译器 :一份新 spec 的 AC 经 DSL 合并自动生成 pytest 骨架(带 hash 头);手改生成测试触发 CI 红、改 spec 才放行的实测;spec CI 关卡在 specs/** PR 生效。运行时证据 :编译产物 + tamper 红 + spec PR 全关卡绿。
骨架 fan-out :一次真实卡的 N=3–4 骨架 fan-out 全套产物:分歧正交分解报告(契约分歧 → spec 修订 PR;路线分歧 → 策略菜单)、测试草案交集入 AC 记录、假设清单并集、趋同度/分歧率入 metrics。运行时证据 :骨架文件 + 机械计算日志 + metrics + (若有)spec 修订 PR。
C 组(实现 fan-out、oracle 与燃料管道)
fan-out + early-exit :试点卡 N=3 实现并行,首个过全 gate 者即时合并(early-exit 时间线可查),其余转后台;决策矩阵对一张低决策密度卡自动打"免 fan-out"标签。运行时证据 :三条 PR 时间线 + 标签记录。
champion/oracle :跨簇亚军冻结为 oracle 的记录;champion-oracle 对拍常驻运行(硬区/软区边界标注);一次注入分歧被裁决(bug 修复或修宪路由)的记录;(如发生)性能更优者经对拍+全 gate 替换 champion 的 improvement PR。运行时证据 :oracle 冻结记录 + 对拍运行历史 + 裁决记录。
燃料管道 :一次真实红队 run 消费 fan-out 产物的全链记录(淘汰路线 → 差异攻击查询机械生成 → CNB 候选生成 → 机械核对 → 判定);意图道闸消费假设清单的留痕(含一次 S6–S8 命中或"无命中"落盘)。运行时证据 :fanout JSONL 产物 + 适配器日志 + 红队 run 链接。
D 组(CNB 底座)
接缝审计 :治理仓 grep CNB 仅命中三接缝;cnb-bridge 结构齐全。运行时证据 :审计命令输出。
配额 :dashboard 每账号余量/消耗/外推耗尽日;<20% 注入告警一次;1C 档任务 build logs 出现 cpus=1。运行时证据 :metrics + 告警 + build 记录。
陌生 AI 入职 :未参与开发的 AI 仅凭 runbook 完成真实入职,lifecycle 留痕。运行时证据 :lifecycle + canary 记录。
强模型 7 天 :有活日产出无撞车,无活日零误派单仅心跳。运行时证据 :work-inbox 历史 + 会话记录。
试点卡端到端 :条 9+10+11+12 全链一次打通,人类触点 = 1+1;NPC 产物机械核对零作废进判定。运行时证据 :卡时间线 + PR 链。
周审计 :连续 4 周自动 issue 五项齐全;一次注入红项触发 CNB_DISABLED 建议。运行时证据 :issue 链。
E 组(演练与 token)
演练全自动 :月度干跑零人工;季度功能演练全程自动(置位→fallback 真实任务→gate 绿→复位→计时),人工参与度 = 0。运行时证据 :演练 issue + 计时 + fallback run 链接。
token ADR :决策与缓解条款合并。运行时证据 :ADR diff + secret 存在性查询。
非目标(NONGOAL)
不追求全仓形式化——只条件触发"小而稳定而高危"的面;checklist 判不适用即不启动,不为跑而跑
不重写存量 spec 为 DSL(新增起强制,存量自然迁移)
不自研模糊/变异/符号/形式化框架——全部接现有工具,本 IR 只做接入、生成侧、触发条件与裁决锚点
不做无停止规则的无限 fan-out:N 默认 3–4;趋同卡自动获"免 fan-out"标签;top-2 差距小于选择器判别力时升级选择器而非加大 N;N>16 需 ADR 特殊理由
不给所有卡强制 fan-out——决策矩阵 gating,低决策密度×高可判定 = 单实例+机械门禁
不把 oracle 当产品维护——只换代不修补;不修补污染独立性
不迁移 SSOT 到 CNB;不做镜像同步与"停摆周"(后续卡片)
不依赖 api_trigger(未开放,留月度复验探针);不做多平台抽象层;不自研 CNB SDK
不修改判定语义:testing.yaml 既有条款语义、gate/org-gate 结构、conductor/arbiter 状态机零变化(新增条款与 checkpoint 为增量)
不把 NPC/LLM 输出直接作为任何 gate 输入——一切经机械锚点
不做物理删除演习(owner 裁决:一次性退休动作,接受证明力降低换零人工)
约束 / 不可违反项
临时措施总原则 :一切 CNB 内容可整体删除;判定链不经过 CNB 是架构不变式——任何把 CNB 写进判定路径的改动即违约。
生成/裁决分离 :变异分数、测试通过、覆盖率、DSL hash、栈哈希去重、骨架交集/并集、fan-out 选择器裁决、kernel 检查——全部 GitHub CI 内代码核算;沙箱自报数字一律不采信。
机械核对铁律 :NPC 产物进判定链前必经机械核对(基准 SHA run 开始时动态获取并写入报告——IR: 卡绑定测试与红队守门制度(LLM-as-a-Verifier 验证 + 意图兜底道闸) #263 erratum 为鉴;diff 可 apply;输出格式校验);不符 = 作废记 infra 失败。燃料管道产物同受此铁律 :fan-out 产物进红队/道闸输入前过 SHA 基准锚定核对;红队输入适配器只读结构化产物目录(管道即接口)。
弱模型判断的结构化前提 (条 7):checklist 是机器可读 YAML、C1 路径文件;判断输出逐项留痕入卡(可审计可重放);凡卡元数据可机械判定的字段优先纯脚本,弱模型只填语义字段;checklist 本身是人类一次性投入,修改走 ADR。
风险等级 fail-closed (条 7):risk_level 缺失的卡/spec 不得进入形式化触发判定——按触发处理或退回补全,二选一由 policy 配置。
fan-out 纪律 :early-exit 不跳过任何 gate;champion 替换必须 oracle 对拍 + 全 gate 双重裁决;oracle 只换代不修补;champion-oracle 硬区分歧未裁决前暂停相关合并;停止规则由 policy 配置。
骨架/实现分离测不同的方差 :spec 阶段测解读方差(歧义),实现阶段测解的方差(难度)——两台仪器不混用;骨架 fan-out 产物是测量仪器(交集/并集/分歧分解全机械计算),LLM 只产骨架本身。
既有护栏全部适用 :派单前检查 AUTO_MERGE_DISABLED 与 cost 熔断;auto-fix ≤3 对 CNB 派单同样计数。
凭据纪律 :CNB token 只存 org secret;任务文本不含凭据与敏感内容;NPC 沙箱不注入 GitHub 凭据;高权限 token 风险由 ADR 缓解条款覆盖。
窗口纪律 :投递前二次确认最后评论归属;快占快放;单账号并发 ≤8;任务带 run-id 前缀。
C1 路径 :EX-1、automation-limits 新节、两个 workflow、testing.yaml 新条款、X-04 修订 ADR、token ADR、卡模板 risk_level 字段——PR + ADR 引用 + owner merge。
账本不可改写 :usage 账本、lifecycle.jsonl、triage ledger、fanout 产物 JSONL 均 append-only;纠错 = 追加 erratum 行。
DSL 溯源不可绕过 :生成测试的 spec hash 校验是 gate 级检查;豁免只能走 ADR(escape_hatch 同 T-13 模式)。
强模型会话幂等 :lease + 清单 id 去重。
观测口径以 CNB 为准 :核·秒以 build logs(duration×labels.cpus)为对账真源。
人类愿意接受的验收证据
二十条期望变化各自的运行时证据(见各条加粗段)
机械裁决记录样本 :变异裁判日志、骨架交集/并集计算日志、kernel 二值结果、DSL tamper 红、崩溃去重指纹、燃料管道适配器日志——证明"生成侧放了 AI,裁决侧没放"
一次形式化自动触发全链(弱模型判断日志 → kernel 结果)与一次判"不适用"留痕
陌生 AI 入职实录与强模型 7 天运行记录——可交接性证明
一次全自动功能演练计时与 fallback run 链接
配置面证据:accounts.yaml + automation-limits cnb 节 + testing.yaml 新条款 + 决策矩阵/checklist/停止规则配置——账号、测试、fan-out 的扩张均为配置行为
可逆性偏好
CNB 整层可删(kill-switch 功能演练周期证明);A 组各方法可独立停用(条款移除即回退);formal checklist 可把触发门槛收紧至等效 X-04(永不触发);fan-out 各模式可独立关停(回退单实例+机械门禁);oracle 可退役(退役记录入账);燃料管道可关停(红队回退读 spec 原文);DSL 对存量无迁移义务;单账号可独立 draining;任何回退不影响已合并卡历史与判定记录。
质量-速度旋钮
质量不降级面:机械裁决全部(分数核算、hash 溯源、栈哈希、交集/并集、kernel、对拍、燃料核对)、账本真实性、审计五项、幂等语义、early-exit 不跳 gate。可调面:深跑时长与档位(配额紧张先降 cpus/并发)、审计抽样比例(10% 可降不可免)、试点范围、fan-out 的 N 值与模式(默认 3–4,收敛带宽紧张时先降 N)、oracle 保有数量、formal 触发的风险等级门槛(可收紧不可静默放宽)。配额耗尽或 CNB 失效时系统行为 = 清单挂起 + fallback + 开 issue,永不 为跑完而跳过记账、核对或机械裁决。
job(要完成的待办)
一次补全验证体系的既有缺口,并以 CNB 免费算力(CodeBuddy NPC 沙箱,每账号 1600 核时/月)作为发散侧底座。两条贯穿原则:
A. 测试方法缺口闭环(对 quality 纲要差距报告的逐项落实)
go test -fuzz长轮)放 CNB 沙箱(低档位长跑,省 GitHub runner);崩溃样本机械去重(栈哈希)后 LLM 仅写分诊草稿(人/机械裁决);锚点(唯一崩溃数、覆盖率增量)在 GitHub CI 汇总核算,不采信沙箱自报数字。a. 结构化适用性 checklist(机器可读 YAML,C1 路径文件):正适用项(有清晰数学定义的算法核心 / 可建状态机的协议逻辑 / 密码原语 / 高风险且稳定的核心小块)与反适用项(无法脱离环境描述的胶水 / 无半形式化规范起点 / 演进中的契约 / 循环深度无界)+ 风险等级门槛(业务输入,"这段代码错了要赔多少钱")——checklist 判断由弱模型(或纯脚本,凡卡元数据可机械判定的字段优先机械)按卡/spec 元数据执行,逐项判断与理由留痕入卡,可审计可重放;
b. 自动启动管线:checklist 判"适用"即自动启动形式化作业(工具按栈选型并试点实测:算法核用 Dafny/crosshair 类、状态机用 TLA+ 类),kernel 检查为唯一锚点,证明通过/失败二值回写卡的验证面板;
c. 试点实跑:aws-tb 挑 1–2 个正适用目标(判分算法核心、某状态机)真实跑通一次 kernel 检查全链(checklist 触发→作业→二值结果)。
卡/spec 模板新增
risk_level字段(owner/业务显式给定;缺失 = fail-closed 按触发处理或退回补全)。B. spec 的 CI 与 spec 质量测量(不止 lint)
C. 实现 fan-out、champion/oracle 生命周期与燃料管道(测"解的方差")
D. CNB 免费算力底座(临时措施、可删除层、发散侧专用)
Cloudbird-Software/cnb-bridge(L2,public):多账号调度器、派单协议、配额账本、账号 runbook、work-inbox 全部集中于此;核心治理对 CNB 的引用收敛为三接缝:GOVERNANCE.yaml EX-1 条目、org secrets(CNB_TOKEN_<alias>)、两个 workflow(cnb-dispatch / cnb-audit);REMOVAL.md 单页删除清单。charge/quota定时快照 +build/logs实耗对账 → append-only 账本 → 既有 metrics.py 仪表盘;余量 <20% 自动开 cost-infra issue;对账偏差 >10% 告警;账号与档位阈值全部是配置(automation-limits.yaml 新节cnb:),加账号=改配置零代码;档位 light=1C(默认)/ std=2C / heavy=4C(须理由),8C 禁用,派单必填档位。cnb-bridge/work-inbox.yaml为强模型每小时自起的唯一工作发现入口——有 pending → 带 lease 认领 → 产出 → 写回释放;无 pending → 心跳行退出。lease 超时自动过期;清单 id 去重保证重复会话不重复派单。E. 可脱离性演练(全自动)与 token 决策
CNB_DISABLED→ 发散链全量切 fallback 付费 API 跑一轮真实任务 → gate 全绿 → 自动复位 → 计时报告)。物理删除为一次性退休动作,不做演习;证明力边界如实入册(owner 裁决:接受证明力降低换零人工)。触发场景
当前痛点的证据
期望的可观察变化(验收时能在线上看到的事实)
A 组(测试缺口)
B 组(spec 的 CI 与质量测量)
C 组(实现 fan-out、oracle 与燃料管道)
D 组(CNB 底座)
cpus=1。运行时证据:metrics + 告警 + build 记录。E 组(演练与 token)
非目标(NONGOAL)
约束 / 不可违反项
人类愿意接受的验收证据
可逆性偏好
CNB 整层可删(kill-switch 功能演练周期证明);A 组各方法可独立停用(条款移除即回退);formal checklist 可把触发门槛收紧至等效 X-04(永不触发);fan-out 各模式可独立关停(回退单实例+机械门禁);oracle 可退役(退役记录入账);燃料管道可关停(红队回退读 spec 原文);DSL 对存量无迁移义务;单账号可独立 draining;任何回退不影响已合并卡历史与判定记录。
质量-速度旋钮
质量不降级面:机械裁决全部(分数核算、hash 溯源、栈哈希、交集/并集、kernel、对拍、燃料核对)、账本真实性、审计五项、幂等语义、early-exit 不跳 gate。可调面:深跑时长与档位(配额紧张先降 cpus/并发)、审计抽样比例(10% 可降不可免)、试点范围、fan-out 的 N 值与模式(默认 3–4,收敛带宽紧张时先降 N)、oracle 保有数量、formal 触发的风险等级门槛(可收紧不可静默放宽)。配额耗尽或 CNB 失效时系统行为 = 清单挂起 + fallback + 开 issue,永不为跑完而跳过记账、核对或机械裁决。