agentsclimarketplace

Proofreader skill

Skill easyzoom/proofreader-skill

SKILL.md-standard proofreading skill — code & document review with real, verified formal-verification backends for C, Python, Rust, Java, and C++

Install
npx -y skills add easyzoom/proofreader-skill

Assembled from the repository path, not quoted from the project. Check it against their README if it does not work.

2 things to look at

  • 25 days oldThe repository was created 25 days ago. New is not bad, but a brand new repository carrying a familiar-sounding name is the shape a typosquat arrives in, and there has been no time for anyone else to find a problem with it.
  • 1 stars1 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.

What its author says it does

Copied from the file, not written here

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

The file declares its own license as MIT. That is the author’s claim about this one file, and it is not the same thing as the license GitHub reports for the repository, which is listed with the other numbers below.

SKILL.md

6.0 KB, as published. Nobody here has run it

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] harnessreferences/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/ 里的结论、命令、参数没有和工具的真实行为脱节。

Keep looking

Skills are one crate of 328,083. Ordering is by how many stacks a row turns up in, so the top of any crate is what has actually been picked rather than what has the most stars.