Proofreader
通用校对能力,包含两条并行且同等重要的主线:代码校对 和 文档校对。先判断输入属于哪一类,再进入对应流程;两者都涉及时,分别过一遍。
第一步:分类
- 输入主要是源代码(任意语言) → 进入「代码校对」
- 如果代码语言在下面的「语言特定形式化验证后端」列表里,且代码里出现对应的契约/规约标记 → 额外启用对应后端(可能不止一种,比如既有 ACSL 注释又想找具体反例)
- 否则(或者没有工具支持的语言/没写契约)走通用代码逻辑审查 →
references/code-proofreading.md
- 输入主要是自然语言文档/文本(任意语言) → 进入「文档校对」→
references/doc-proofreading.md
- 两者都有(例如 README + 代码示例)→ 分别执行两条流程
语言特定形式化验证后端
| 语言 |
契约/规约标记 |
静态证明 |
运行时验证/找反例 |
| C |
/*@ ... */ 或 //@,含 requires/ensures/assigns/invariant 等 |
references/acsl-frama-c.md(Frama-C WP) |
references/eacsl-runtime.md(E-ACSL) |
| Python |
@icontract.require/@icontract.ensure 装饰器 |
references/python-contracts.md(CrossHair,注意不是穷尽证明) |
references/python-contracts.md(icontract 运行时检查) |
| Rust |
用户明确要求验证,或代码里已有 #[kani::proof] harness |
references/rust-kani.md(Kani,无循环代码是穷尽式,含循环需查展开界限) |
同上(Kani 一次跑同时覆盖) |
| Java |
//@ 或 /*@ ... */ 注释,含 requires/ensures/invariant 等(JML) |
references/java-openjml.md(OpenJML -esc) |
同上(OpenJML 同一个命令一次跑完) |
| C++ |
用户明确要求验证(没有成熟的 ACSL for C++ 标准) |
references/cpp-cbmc.md(CBMC,无循环代码是穷尽式,含循环需查展开界限,和 Kani 同理) |
同上(CBMC 一次跑同时覆盖) |
每种后端都遵循同一个模式:契约本身要先人工校对(规约是否写全、写对),再实际调用工具验证,不要仅凭肉眼判断。跑工具前先检查工具是否已安装,缺失就如实告知并给出安装方式,不要假装验证过。
代码校对总原则
- 不只看语法和风格,要追踪数据流/控制流,找真正会在具体输入或状态下触发的问题,而不是泛泛的"风格建议"。
- 每个发现都要给出:文件位置、触发场景(什么输入/状态下出错)、以及现有代码为什么没有覆盖这种情况。
- 有工具可做形式化验证时,优先实际跑工具得出结论,不要仅凭肉眼判断规约/契约是否成立——静态证明和运行时检查都比人工推演可靠,但要注意不同工具的严格程度不同(例如 Frama-C/WP 是穷尽式数学证明,CrossHair 只是有限预算内的符号搜索,不能混为一谈,具体差异见对应 reference 文件)。
文档校对总原则
见 references/doc-proofreading.md。核心是语法正确性、术语一致性、跨语言表达自然度、格式规范,不擅自改写作者的行文风格。
参考文件
references/code-proofreading.md — 通用代码逻辑校对方法论(不限语言)references/acsl-frama-c.md — ACSL 规约校对 + Frama-C 静态证明调用方法(C)references/eacsl-runtime.md — E-ACSL 运行时验证调用方法(C)references/python-contracts.md — icontract 契约校对 + CrossHair 符号执行调用方法(Python)references/rust-kani.md — Kani 有界模型检验调用方法(Rust)references/java-openjml.md — JML 规约校对 + OpenJML -esc 调用方法(Java)references/cpp-cbmc.md — CBMC 有界模型检验调用方法(C++)references/doc-proofreading.md — 多语言文档校对方法论
实测案例(每条主线都有真实验证过的案例,不是预期描述)
examples/abs-int/ — C + ACSL:abs_int(INT_MIN) 溢出 bug,WP 静态证明 + E-ACSL 运行时验证的完整闭环examples/python-contracts/ — Python + icontract:first_index_ge 的 off-by-one 漏报 bug,CrossHair 找反例 + icontract 运行时验证的完整闭环examples/rust-kani/ — Rust + Kani:add_percentage 的中间乘法溢出 bug,Kani 有界模型检验的完整闭环examples/java-openjml/ — Java + JML:abs(Integer.MIN_VALUE) 溢出 bug,和 C 那个几乎是同一个 bug,OpenJML -esc 静态验证的完整闭环examples/cpp-cbmc/ — C++ + CBMC:FixedStack 固定容量容器越界写入 bug,CBMC 有界模型检验的完整闭环examples/code-proofreading/ — 通用代码校对:merge_intervals 对未排序输入静默丢数据的真实 bugexamples/doc-proofreading/ — 文档校对:一份混入 6 类真实问题(语法/格式/重音符号/术语不一致/逻辑矛盾)的示例文档 + 校对报告 + 修正版
scripts/verify.sh 会重新校验 SKILL.md 是否仍符合 Agent Skills 规范,并重跑上述案例,确认 references/ 里的结论、命令、参数没有和工具的真实行为脱节。
1---2name: proofreader-skill3description: Use when asked to proofread, review, or 校对 code or documents for correctness, logical consistency, or quality issues. Covers general code logic review (any language), plus formal-verification backends for C (ACSL contracts via Frama-C static proof and E-ACSL runtime checks), Python (icontract + CrossHair), Rust (Kani bounded model checking), Java (JML + OpenJML), and C++ (CBMC), as well as multi-language document/text proofreading (grammar, terminology, consistency). Triggers on "proofread", "校对", "review this file/PR/doc", "check for bugs/inconsistencies", "verify ACSL/JML annotations", "run frama-c", "run e-acsl", "verify with kani", "run crosshair", "run openjml", "run cbmc".4license: MIT5---67# Proofreader89通用校对能力,包含两条并行且同等重要的主线:**代码校对** 和 **文档校对**。先判断输入属于哪一类,再进入对应流程;两者都涉及时,分别过一遍。1011## 第一步:分类1213- 输入主要是源代码(任意语言) → 进入「代码校对」14 - 如果代码语言在下面的「语言特定形式化验证后端」列表里,且代码里出现对应的契约/规约标记 → 额外启用对应后端(可能不止一种,比如既有 ACSL 注释又想找具体反例)15 - 否则(或者没有工具支持的语言/没写契约)走通用代码逻辑审查 → `references/code-proofreading.md`16- 输入主要是自然语言文档/文本(任意语言) → 进入「文档校对」→ `references/doc-proofreading.md`17- 两者都有(例如 README + 代码示例)→ 分别执行两条流程1819### 语言特定形式化验证后端2021| 语言 | 契约/规约标记 | 静态证明 | 运行时验证/找反例 |22|---|---|---|---|23| C | `/*@ ... */` 或 `//@`,含 `requires`/`ensures`/`assigns`/`invariant` 等 | `references/acsl-frama-c.md`(Frama-C WP) | `references/eacsl-runtime.md`(E-ACSL) |24| Python | `@icontract.require`/`@icontract.ensure` 装饰器 | `references/python-contracts.md`(CrossHair,注意不是穷尽证明) | `references/python-contracts.md`(icontract 运行时检查) |25| Rust | 用户明确要求验证,或代码里已有 `#[kani::proof]` harness | `references/rust-kani.md`(Kani,无循环代码是穷尽式,含循环需查展开界限) | 同上(Kani 一次跑同时覆盖) |26| Java | `//@` 或 `/*@ ... */` 注释,含 `requires`/`ensures`/`invariant` 等(JML) | `references/java-openjml.md`(OpenJML `-esc`) | 同上(OpenJML 同一个命令一次跑完) |27| C++ | 用户明确要求验证(没有成熟的 ACSL for C++ 标准) | `references/cpp-cbmc.md`(CBMC,无循环代码是穷尽式,含循环需查展开界限,和 Kani 同理) | 同上(CBMC 一次跑同时覆盖) |2829每种后端都遵循同一个模式:契约本身要先人工校对(规约是否写全、写对),再实际调用工具验证,不要仅凭肉眼判断。跑工具前先检查工具是否已安装,缺失就如实告知并给出安装方式,不要假装验证过。3031## 代码校对总原则32331. 不只看语法和风格,要追踪数据流/控制流,找真正会在具体输入或状态下触发的问题,而不是泛泛的"风格建议"。342. 每个发现都要给出:文件位置、触发场景(什么输入/状态下出错)、以及现有代码为什么没有覆盖这种情况。353. 有工具可做形式化验证时,优先实际跑工具得出结论,不要仅凭肉眼判断规约/契约是否成立——静态证明和运行时检查都比人工推演可靠,但要注意不同工具的严格程度不同(例如 Frama-C/WP 是穷尽式数学证明,CrossHair 只是有限预算内的符号搜索,不能混为一谈,具体差异见对应 reference 文件)。3637## 文档校对总原则3839见 `references/doc-proofreading.md`。核心是语法正确性、术语一致性、跨语言表达自然度、格式规范,不擅自改写作者的行文风格。4041## 参考文件4243- `references/code-proofreading.md` — 通用代码逻辑校对方法论(不限语言)44- `references/acsl-frama-c.md` — ACSL 规约校对 + Frama-C 静态证明调用方法(C)45- `references/eacsl-runtime.md` — E-ACSL 运行时验证调用方法(C)46- `references/python-contracts.md` — icontract 契约校对 + CrossHair 符号执行调用方法(Python)47- `references/rust-kani.md` — Kani 有界模型检验调用方法(Rust)48- `references/java-openjml.md` — JML 规约校对 + OpenJML `-esc` 调用方法(Java)49- `references/cpp-cbmc.md` — CBMC 有界模型检验调用方法(C++)50- `references/doc-proofreading.md` — 多语言文档校对方法论5152## 实测案例(每条主线都有真实验证过的案例,不是预期描述)5354- `examples/abs-int/` — C + ACSL:`abs_int(INT_MIN)` 溢出 bug,WP 静态证明 + E-ACSL 运行时验证的完整闭环55- `examples/python-contracts/` — Python + icontract:`first_index_ge` 的 off-by-one 漏报 bug,CrossHair 找反例 + icontract 运行时验证的完整闭环56- `examples/rust-kani/` — Rust + Kani:`add_percentage` 的中间乘法溢出 bug,Kani 有界模型检验的完整闭环57- `examples/java-openjml/` — Java + JML:`abs(Integer.MIN_VALUE)` 溢出 bug,和 C 那个几乎是同一个 bug,OpenJML `-esc` 静态验证的完整闭环58- `examples/cpp-cbmc/` — C++ + CBMC:`FixedStack` 固定容量容器越界写入 bug,CBMC 有界模型检验的完整闭环59- `examples/code-proofreading/` — 通用代码校对:`merge_intervals` 对未排序输入静默丢数据的真实 bug60- `examples/doc-proofreading/` — 文档校对:一份混入 6 类真实问题(语法/格式/重音符号/术语不一致/逻辑矛盾)的示例文档 + 校对报告 + 修正版6162`scripts/verify.sh` 会重新校验 `SKILL.md` 是否仍符合 Agent Skills 规范,并重跑上述案例,确认 references/ 里的结论、命令、参数没有和工具的真实行为脱节。
easyzoom