diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 46b8149..f550395 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -16,9 +16,39 @@ lake build
 
 ## Branching
 
-- `main` — stable releases / published tip  
-- `development` — integration branch  
-- Feature work: branch from `development` (e.g. `feature/…`)
+Flow: **`feature/…` → `development` → `main`**. GitHub rulesets require a pull request (and green CI) into `development` and `main`. Direct pushes to those branches are not part of the workflow.
+
+| Branch | Role |
+|---|---|
+| `feature/…` | All implementation work (branch from latest `development`) |
+| `development` | Integration / staging tip — **PR only** from `feature/…` |
+| `main` | Stable / published tip — **PR only** from `development` |
+| tags `v*` | Releases — created on `main` only (see [packaging.md](docs/packaging.md)) |
+
+### How to land a change
+
+```bash
+git fetch origin
+git checkout development && git pull origin development
+git checkout -b feature/<short-name>
+# … commit …
+git push -u origin HEAD
+gh pr create --base development --title "…" --body "…"
+```
+
+1. Wait for CI on the feature PR (`build-test`, `stress-framing`, `interop-grpc-go`, `interop-python`, `interop-rust`, `h2spec`).
+2. Merge into `development`.
+3. When ready to publish the tip, open **`development` → `main`** (prefer a merge that keeps `main` a clean promote of `development`; squash only for a single logical promote if needed).
+4. Tag releases from `main` only — maintainers, manually ([packaging.md](docs/packaging.md)).
+
+### Do not
+
+- Open PRs from `feature/*` directly into `main`
+- Commit or push straight to `main` or `development`
+- Force-push `main` or `development`
+- Create or push release tags from agents/CI
+
+Agents and humans follow the same path.
 
 Release / Reservoir checklist (tagging is **manual**): [docs/packaging.md](docs/packaging.md).
 
@@ -114,10 +144,11 @@ User docs live under [`docs/`](docs/README.md) (source of truth). Curated pages
 
 ## Pull requests
 
-1. Clear description of *why* and how to test.
-2. Green CI on the PR branch.
-3. No unrelated refactors.
-4. Do not force-push `main` / `development` unless maintainers ask.
+1. Base branch must be **`development`** for feature work (never `main`).
+2. Clear description of *why* and how to test.
+3. Green CI on the PR branch.
+4. No unrelated refactors.
+5. Do not force-push `main` / `development`.
 
 ## License
 
diff --git a/docs/packaging.md b/docs/packaging.md
index 9b23819..82a60b9 100644
--- a/docs/packaging.md
+++ b/docs/packaging.md
@@ -82,7 +82,7 @@ Package version in-tree is **1.1.0** (`lakefile.lean`, `Grpc.version`). Hosted d
 
 Documented only — do **not** automate tagging from CI or agent runs.
 
-1. Merge packaging / feature work → `development`, then promote to `main` when ready to publish.
+1. Land packaging / feature work via PR into `development`, then promote with PR **`development` → `main`** when ready to publish.
 2. Confirm the repository is **public** and GitHub license detection shows **Apache-2.0**.
 3. Enable GitHub Security Advisories / private vulnerability reporting if available.
 4. Obtain **≥2 GitHub stars** ([Reservoir inclusion criteria](https://reservoir.lean-lang.org/inclusion-criteria)).
@@ -104,8 +104,15 @@ Documented only — do **not** automate tagging from CI or agent runs.
 
 ## Branching
 
-- `main` — stable releases / published tip  
-- `development` — integration  
-- `feature/…` — branch from `development`
+Flow: **`feature/…` → `development` → `main`** (enforced with GitHub rulesets: PR + green CI into `development` and `main`).
 
-See also [CONTRIBUTING.md](../CONTRIBUTING.md) and [CHANGELOG.md](../CHANGELOG.md).
+| Branch | Role |
+|---|---|
+| `feature/…` | Implementation; branch from `development`; direct push allowed |
+| `development` | Integration tip; **PR only** from `feature/…` |
+| `main` | Published tip; **PR only** from `development` |
+| tags `v*` | Releases; create on `main` only |
+
+Do **not** open `feature/*` → `main` PRs, commit directly to `main`/`development`, or force-push those branches. Full contributor steps: [CONTRIBUTING.md](../CONTRIBUTING.md).
+
+See also [CHANGELOG.md](../CHANGELOG.md).