Tooling

Hooks and configs that validate CKC commit messages live in a separate repository, hotherio/ckc-tools. They are built to run alongside existing Conventional Commits tooling, not replace it.

The collision, and how to avoid it

A strict Conventional Commits validator allows only a fixed list of types, so it rejects CKC types such as formalize and experiment. Because CKC is a superset, a CKC validator already accepts every plain Conventional Commit (feat, fix, docs). The rule is simple: never run two validators with disjoint type lists. A repository that holds both a paper and its proofs uses the CKC validator and nothing conflicts, since it accepts both plain Conventional Commits for tooling and CKC commits for the work.

What is available

• ckc-lint, a commit-msg validator (Python, no Node). It checks that a message is a valid Conventional Commit and follows CKC: a known type for the active profiles, a known Status: value, uppercase trusted-base markers, ~ consistency, and well-formed relation footers.
• ckc-axiom-check, an opt-in honesty hook for the proof profile. When a commit claims Status: math.machine-checked, it cross-checks the named Lean: declarations against the kernel via the lean-math axiom-report and rejects the commit if the kernel disagrees.
• commitlint-config-ckc, a commitlint shareable config for the JavaScript world that widens type-enum to the CKC vocabulary.

For AI agents

Three artifacts teach agents to write and validate CKC commits, so the convention is followed without being restated each time. From reference to procedure to tooling:

• llms.txt, the condensed machine-readable spec at the site root. The reference every other artifact points to.
• The community skill, a tool-agnostic SKILL.md hosted on this site (CC BY 4.0). It carries the grammar, both status ladders, the authoring procedure, and the statement-fidelity discipline (rule 14), with no assumption about which proof assistant, lab, or validator you use. Drop it into any repository or agent that reads skills.
• The conventional-knowledge-commits skill, a Claude Code plugin shipped in hotherio/ckc-tools and invoked as /ckc:conventional-knowledge-commits, plus a portable AGENTS.md for the agents that read that convention (Cursor, Codex, Aider, Continue). These are tooling-integrated: they carry the ckc-lint, ckc-axiom-check, and claimgraph commands and read the vocabulary from vocab.json, so they stay in step with the spec.

Profiles

A repository chooses which profiles are active: proof, science, or both (the default). With one profile active, a type from the other profile is rejected. Set it with the --profile flag, $CKC_PROFILES, or a .ckc.toml at the repo root:

# .ckc.toml
profiles = ["proof"]   # or ["science"], or ["proof", "science"]

With the pre-commit framework

For a repository with no Conventional Commits hook yet, ckc alone validates both Conventional Commits and CKC:

# .pre-commit-config.yaml
repos:
  - repo: https://github.com/hotherio/ckc-tools
    rev: v0.1.3
    hooks:
      - id: ckc

pre-commit install --hook-type commit-msg

The id ckc is also available as conventional-knowledge-pre-commit, an alias named to parallel conventional-pre-commit. Both ids run the same validator.

ckc is a drop-in superset of conventional-pre-commit: it accepts the same interface (positional types, --strict, --force-scope, --scopes, --no-color, --verbose, exit codes 0 and 1, and fixup!/merge commits passing unless --strict), and additionally allows the CKC vocabulary and runs the CKC checks. You have two options.

Migrate to ckc only

Drop conventional-pre-commit and keep your existing args: change the repo and id, and the rest carries over (a pinned type list is still honoured exactly; remove it to allow the full CKC vocabulary).

- repo: https://github.com/hotherio/ckc-tools
  rev: v0.1.3
  hooks:
    - id: ckc
      stages: [commit-msg]
      args: [--strict, --scopes, "api,client"]   # the same args you gave conventional-pre-commit

Or keep conventional-pre-commit

If you prefer to keep it, run ckc next to it and widen conventional-pre-commit's allowed types so it stops rejecting CKC types. Generate the list with ckc-lint --print-types (it respects the active profiles) and paste it into the hook's args. Both hooks run on commit-msg; neither is replaced.

With lefthook

# lefthook.yml
commit-msg:
  commands:
    ckc:
      run: ckc-lint {1}

lefthook passes the commit message file as {1}. Install ckc-lint (pip install git+https://github.com/hotherio/ckc-tools) first.

With commitlint

// commitlint.config.js
module.exports = {
  extends: ['@commitlint/config-conventional', 'commitlint-config-ckc'],
};

commitlint-config-ckc extends config-conventional and only widens the type list, so it runs alongside a conventional setup rather than replacing it.

The honesty hook

ckc-axiom-check extends the lean-math working-tree honesty gate into the commit log. It acts only on a commit that claims math.machine-checked or math.axiomatised and names Lean: declarations, and it rejects only a genuine contradiction (the kernel reports a sorryAx or a cited axiom while the commit claims machine-checked). It needs Lean, a built project, and axiom-report on PATH (or $CKC_AXIOM_REPORT); when it cannot determine a declaration's status it skips.

Since ckc-tools v0.3.0 the hook also enforces rule 14: a math.axiomatised commit is rejected unless it carries Source-Ref: and Refutation-Attempt: footers, and ckc-lint warns on the same gap in repositories that do not run the hook. The earlier token spelling Paper-Ref: is accepted as a deprecated alias for one release.

See hotherio/ckc-tools for the full readme and the single-source vocabulary (vocab.json) shared by the Python validator and the commitlint config.