English · Español · Português · Deutsch · Français · 简体中文 · 繁體中文 · 한국어 · 日本語 · Русский · Türkçe

proofreader-skill

A general-purpose proofreading skill written to the Agent Skills open standard (SKILL.md format). Drop it into any tool that supports the standard (Claude Code, Codex CLI, Gemini CLI, etc.) and use it directly.

Cross-tool loading has been empirically tested with Codex CLI: given its installed-skills list, it correctly picked proofreader-skill for an ACSL-proofreading task and cited the exact trigger keywords from SKILL.md's description. Compatibility with other tools follows from passing skills-ref validate (official Agent Skills spec compliance) but hasn't been individually tested tool by tool.

This README is the human-facing project description. What actually drives the AI's behavior is SKILL.md and the detail docs under references/.

What this skill does

Two parallel, equally important capabilities:

1. Code proofreading — general code logic review (any language), plus dedicated formal-verification backends for specific languages:
   • C + ACSL: Frama-C's WP plugin does static proof of ACSL contracts (requires/ensures/assigns/loop invariants, etc.); E-ACSL translates the same annotations into runtime checks, verified during actual execution — a violation yields a concrete counterexample
   • Python: icontract decorators check contracts at runtime; CrossHair does symbolic execution to search for a counterexample (a bounded search, not an exhaustive proof)
   • Rust: Kani (bounded model checking) verifies a #[kani::proof] harness — exhaustive for loop-free code, bounded for loops/recursion unless the unwind limit is set appropriately
   • Java: JML contracts (//@ requires/ensures, JML's equivalent of ACSL) verified with OpenJML's -esc static checker
   • C++: CBMC (bounded model checking; there's no mature "ACSL for C++") — the same tool family as Kani, just applied directly to C/C++
2. Document proofreading — grammar, terminology consistency, logical consistency, and formatting checks for multilingual text/documents

See the routing logic in SKILL.md for details.

Directory structure

SKILL.md                          Entry point: classification routing (code/doc; code further routes to a per-language verification backend when applicable)
references/
  code-proofreading.md            General code logic proofreading methodology
  acsl-frama-c.md                 ACSL contract review + Frama-C/WP static proof usage (C)
  eacsl-runtime.md                E-ACSL runtime verification usage (C)
  python-contracts.md              icontract contract review + CrossHair usage (Python)
  rust-kani.md                     Kani bounded model checking usage (Rust)
  java-openjml.md                  JML contract review + OpenJML `-esc` usage (Java)
  cpp-cbmc.md                       CBMC bounded model checking usage (C++)
  doc-proofreading.md             Multilingual document proofreading methodology
examples/
  abs-int/                        C+ACSL case study (WP + E-ACSL output is real, executed output)
  python-contracts/                 Python + icontract/CrossHair case study
  rust-kani/                        Rust + Kani case study
  java-openjml/                     Java + JML/OpenJML case study
  cpp-cbmc/                         C++ + CBMC case study
  code-proofreading/               General code proofreading case study
  doc-proofreading/                Document proofreading case study
scripts/
  verify.sh                       Regression check: re-runs the examples above to catch doc/tool drift

Usage

The npx skills add route below requires this repo to be published to a publicly reachable git repository (e.g. GitHub) first. Until it's pushed to a remote, use manual clone/copy instead.

One-line install (recommended, cross-tool) — via the Vercel skills CLI:

npx skills add <owner>/proofreader-skill -a claude-code
# supported -a targets include claude-code, opencode, etc. — see the skills CLI docs for the current list

Manual install: drop the whole repo into the skills directory your tool expects. The directory name must stay proofreader-skill (the Agent Skills spec requires the name field in SKILL.md to match the parent directory name; verify with npx skills-ref validate <path>):

# Claude Code
cp -r proofreader-skill ~/.claude/skills/proofreader-skill

# Codex CLI / other SKILL.md-compatible tools
# follow that tool's own skills-directory convention, keeping the directory name unchanged

Setting up the formal-verification backends

Each language backend needs its own toolchain. Full, actually-executed install-and-verify logs are in each case study's README — real commands and real output, not a description of expected behavior.

C (Frama-C / E-ACSL) — see references/acsl-frama-c.md, references/eacsl-runtime.md, examples/abs-int/README.md. Short version (via opam, not apt — a clean Ubuntu 22.04's apt index may not have a frama-c package):

sudo apt-get install -y opam libgmp-dev libgtksourceview-3.0-dev
opam init -y --disable-sandboxing --bare
opam switch create frama-c 4.14.1
eval $(opam env --switch=frama-c)
opam install -y --assume-depexts frama-c
why3 config detect   # required — otherwise WP fails with "Prover 'Alt-Ergo' not found"

Python (icontract / CrossHair) — see references/python-contracts.md, examples/python-contracts/README.md:

pip3 install --user crosshair-tool icontract

Rust (Kani) — see references/rust-kani.md, examples/rust-kani/README.md:

cargo install --locked kani-verifier
cargo kani setup

Java (OpenJML) — see references/java-openjml.md, examples/java-openjml/README.md. Pick the release build matching your system's glibc/distro (newer releases only ship an Ubuntu 24.04 build; older ones also shipped a 22.04 build) — check that openjml --version actually prints an OpenJML version, not a plain javac version, before trusting its output:

curl -fsSL -o openjml.zip https://github.com/OpenJML/OpenJML/releases/download/<version>/openjml-<your-distro>-<version>.zip
unzip openjml.zip -d openjml && cd openjml
./openjml --version

C++ (CBMC) — see references/cpp-cbmc.md, examples/cpp-cbmc/README.md. Either apt-get install cbmc (needs sudo), or extract the release .deb for your distro without root:

curl -fsSL -o cbmc.deb https://github.com/diffblue/cbmc/releases/download/<version>/<your-distro>-cbmc-<version>-Linux.deb
dpkg-deb -x cbmc.deb ./cbmc-local
export PATH="$PWD/cbmc-local/usr/bin:$PATH"

Status

• SKILL.md's routing logic and all references/ docs are complete; SKILL.md's frontmatter passes the official skills-ref validate check
• Every track (C+ACSL, Python, Rust, Java, C++, general code proofreading, document proofreading) has at least one real, verified case study under examples/
• scripts/verify.sh provides a regression check that re-runs the case studies above and compares against the recorded expected results

Issues and PRs welcome.

License

MIT