| name | proofreader-skill |
| description | 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". |
| license | MIT |
| compatibility | General code/doc proofreading needs nothing extra. Per-language formal-verification backends need their own toolchain — Frama-C/E-ACSL (C), icontract/CrossHair (Python), Kani (Rust), OpenJML (Java), CBMC (C++) — see references/ for install steps. |
| metadata | {"author":"easyzoom.wang","version":"0.1.0"} |
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/ 里的结论、命令、参数没有和工具的真实行为脱节。
