diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 94df8287..275d6c8d 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -3,7 +3,27 @@ We want to make contributing to this project as easy and transparent as
 possible.
 
 ## Our Development Process
-... (in particular how this is synced with internal changes to the project)
+Development happens in this repository: changes reach `main` through pull
+requests. You need Python 3.10 or newer, [`uv`](https://docs.astral.sh/uv/),
+Git, and Make. From a clone:
+
+```bash
+make setup          # uv sync --extra dev --extra repl
+make lint           # uv run ruff check autoform_cli servers tests
+make test           # uv run pytest -q
+make check-example  # validate, render, and build the bundled example site
+```
+
+CI (`.github/workflows/tests.yml`) runs the same four steps on Python 3.10 and
+3.13 for every push and pull request. A separate job runs
+`tests/test_skeleton.py` and one `tests/test_project_inspect.py` test against a
+real Lean toolchain; another runs the inspection, bounded-subprocess, and
+transactional-output tests on Windows. Locally, tests that need Lean skip when
+`lake` is not on `PATH`. The `tests/test_skeleton.py` ones also skip when the
+toolchain pinned in `tests/fixtures/skeleton-project/lean-toolchain` is
+missing; the others let elan download it. Run `lake build` in
+`skills/setup/assets/cabannes-thesis-project` when you change the example's
+Lean sources or declarations.
 
 ## Pull Requests
 We actively welcome your pull requests.
@@ -30,10 +50,14 @@ disclosure of security bugs. In those cases, please go through the process
 outlined on that page and do not file a public issue.
 
 ## Coding Style
-* 2 spaces for indentation rather than tabs
-* 80 character line length
-* ...
+* Python uses 4-space indentation and a 120-character line length
+  (`[tool.ruff]` in `pyproject.toml`). Ruff's default rules do not check line
+  length, and a few existing lines run longer.
+* `make lint` runs `ruff check` with ruff's default rules on `autoform_cli`,
+  `servers`, and `tests`; CI runs the same check.
+* CI runs no formatter, so match the surrounding code instead of reformatting
+  unrelated lines.
 
 ## License
-By contributing to __________, you agree that your contributions will be licensed
+By contributing to autoform-bot, you agree that your contributions will be licensed
 under the LICENSE file in the root directory of this source tree.
diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index ddb6043b..8bc35499 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -114,9 +114,10 @@ This section is the single source of truth for the command line. Skills
 describe what to achieve and link here; they do not restate flags, so a change
 to the CLI lands in one place.
 
-The commands below are written as they appear on `PATH`. Inside a consumer
-project the plugin is not installed, so resolve `<AUTOFORM_PLUGIN_ROOT>` from
-the loaded plugin and prefix each one, running from the project root:
+The commands below are written as they appear on `PATH` once this Python
+package is installed. Inside a consumer project the package is not installed,
+so resolve `<AUTOFORM_PLUGIN_ROOT>` from the loaded plugin and prefix each one,
+running from the project root:
 
 ```bash
 uv run --project "<AUTOFORM_PLUGIN_ROOT>" autoform check blueprint --lean-root .
@@ -680,9 +681,7 @@ worktree each and serialize `lake build` behind a `lake-build` claim, because
 builds share the elan toolchain and the Mathlib cache even when the checkouts
 are separate.
 
-Claims are temporary operational state, never article frontmatter. Future
-Deicyde workers may share this protocol, but their current continue-uncoordinated
-failure behavior must be removed before they use the canonical claim API.
+Claims are temporary operational state, never article frontmatter.
 
 ## Local runtime doctor
 
@@ -706,7 +705,7 @@ This command is strictly read-only and local. It does not invoke Git, GitHub,
 subprocesses, network services, claims, queues, reviews, recovery state,
 providers, workers, renderers, or dashboards, and it creates no cache, scratch
 repository, service, state directory, or `graph.json`. It is a project/runtime
-doctor, separate from any future Deicyde fleet or machine-capability preflight.
+doctor, separate from any future worker fleet or machine-capability preflight.
 
 ## Runtime contract