# Proofreader Skill

> 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".

- Skill: `easyzoom/proofreader-skill` (Agent Skill, multi-file: 15 files)
- Install (CLI): `npx skillmds@latest add easyzoom/proofreader-skill`
- Raw SKILL.md: https://api.skillmd.com/api/skills/easyzoom/proofreader-skill/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- License: MIT
- Author: easyzoom (https://skillmd.com/u/easyzoom)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/easyzoom/proofreader-skill

---


# 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 一次跑同时覆盖) |

每种后端都遵循同一个模式:契约本身要先人工校对(规约是否写全、写对),再实际调用工具验证,不要仅凭肉眼判断。跑工具前先检查工具是否已安装,缺失就如实告知并给出安装方式,不要假装验证过。

## 代码校对总原则

1. 不只看语法和风格,要追踪数据流/控制流,找真正会在具体输入或状态下触发的问题,而不是泛泛的"风格建议"。
2. 每个发现都要给出:文件位置、触发场景(什么输入/状态下出错)、以及现有代码为什么没有覆盖这种情况。
3. 有工具可做形式化验证时,优先实际跑工具得出结论,不要仅凭肉眼判断规约/契约是否成立——静态证明和运行时检查都比人工推演可靠,但要注意不同工具的严格程度不同(例如 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` 对未排序输入静默丢数据的真实 bug
- `examples/doc-proofreading/` — 文档校对:一份混入 6 类真实问题(语法/格式/重音符号/术语不一致/逻辑矛盾)的示例文档 + 校对报告 + 修正版

`scripts/verify.sh` 会重新校验 `SKILL.md` 是否仍符合 Agent Skills 规范,并重跑上述案例,确认 references/ 里的结论、命令、参数没有和工具的真实行为脱节。