diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b996677..6b2107d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -79,7 +79,7 @@ jobs:
       - run: npm run test:action
 
   published-action:
-    name: Action smoke / published v0.5.2
+    name: Action smoke / published v0.5.3
     if: github.event_name == 'push' && github.ref == 'refs/heads/main'
     runs-on: ubuntu-latest
     steps:
@@ -88,7 +88,7 @@ jobs:
         shell: bash
         run: node -e "require('node:fs').appendFileSync('fixtures/demo/base/src/discount.js', '\n// published Action smoke\n')"
       - name: Run ProofDiff from the published repository
-        uses: hzw0813/proofdiff@v0.5.2
+        uses: hzw0813/proofdiff@v0.5.3
         with:
           fail-on: never
           html: published-action-report.html
@@ -97,7 +97,7 @@ jobs:
         run: |
           test -s published-action-report.html
           grep -Fq 'fixtures/demo/base/src/discount.js' published-action-report.html
-          grep -Fq 'Generated locally by ProofDiff 0.5.2' published-action-report.html
+          grep -Fq 'Generated locally by ProofDiff 0.5.3' published-action-report.html
       - uses: actions/upload-artifact@v7
         if: always()
         with:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 470b960..e28ae53 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,7 @@ All notable changes are documented here. This project follows Semantic Versionin
 ### Fixed
 
 - Stopped `.pyi` stub files with test-like names from inventing executable pytest or `unittest` checks. Stubs remain available to static Python analysis and relationship discovery, but framework discovery now requires an executable `.py` test file; this prevents `--run-checks` from launching a Python test runner merely because a repository contains test-shaped type stubs.
+- Updated current stable Action guidance and the published-Action CI smoke from v0.5.2 to the already-released v0.5.3 snapshot, including the immutable full-SHA pin, so documentation and release verification no longer lag the latest public release.
 
 ## [0.5.3] - 2026-08-15
 
diff --git a/README.md b/README.md
index b9effcb..cd8dbcd 100644
--- a/README.md
+++ b/README.md
@@ -105,9 +105,9 @@ Inferred impact and test-like relationships are explicitly labeled static estima
 
 ## Use it in GitHub Actions
 
-The released composite Action is available at `hzw0813/proofdiff@v0.5.2`. Use the released tag for normal stable integration, or the reviewed full commit SHA for an immutable security-sensitive pin. On `pull_request`, the Action can auto-resolve the exact PR base SHA when `base` is omitted; explicit `base` still wins. The released Action includes the `test-map` input for bounded declared relationship data. See the [complete workflow and trust guidance](docs/github-actions.md).
+The released composite Action is available at `hzw0813/proofdiff@v0.5.3`. Use the released tag for normal stable integration, or the reviewed full commit SHA for an immutable security-sensitive pin. On `pull_request`, the Action can auto-resolve the exact PR base SHA when `base` is omitted; explicit `base` still wins. The released Action includes the `test-map` input for bounded declared relationship data. See the [complete workflow and trust guidance](docs/github-actions.md).
 
-For immutable `--base`, `--range`, and `--staged` analysis, v0.5.2 conservatively binds filesystem-backed analysis to the selected Git state instead of mixing snapshots. Base/range analysis requires the selected target to be the checked-out `HEAD`; staged analysis requires tracked worktree content to match the index. Git-visible untracked inputs and ignored metadata/test inputs that could affect static discovery fail closed. With `--run-checks`, ignored repository-local runtime inputs are rejected more broadly because repository commands could consume them; bounded dependency/cache directories remain environment inputs. An explicitly supplied LCOV file can be accepted as that exact data artifact under its separate commit-binding checks, but it does not authorize sibling files.
+For immutable `--base`, `--range`, and `--staged` analysis, v0.5.3 conservatively binds filesystem-backed analysis to the selected Git state instead of mixing snapshots. Base/range analysis requires the selected target to be the checked-out `HEAD`; staged analysis requires tracked worktree content to match the index. Git-visible untracked inputs and ignored metadata/test inputs that could affect static discovery fail closed. With `--run-checks`, ignored repository-local runtime inputs are rejected more broadly because repository commands could consume them; bounded dependency/cache directories remain environment inputs. An explicitly supplied LCOV file can be accepted as that exact data artifact under its separate commit-binding checks, but it does not authorize sibling files.
 
 The released Action writes a concise, bounded **ProofDiff · Change Evidence** job summary by default, so reviewers can see changed-file evidence without opening logs. It uses the same report as terminal/JSON/HTML output, requires no write token, and does not create PR comments. Full provenance remains in the log and optional HTML artifact.
 
diff --git a/docs/github-actions.md b/docs/github-actions.md
index a7e8b6e..ff8881a 100644
--- a/docs/github-actions.md
+++ b/docs/github-actions.md
@@ -16,7 +16,7 @@ jobs:
       - uses: actions/checkout@v7
         with:
           fetch-depth: 0
-      - uses: hzw0813/proofdiff@v0.5.2
+      - uses: hzw0813/proofdiff@v0.5.3
         with:
           fail-on: failed
           html: proofdiff-report.html
@@ -27,16 +27,16 @@ jobs:
           path: proofdiff-report.html
 ```
 
-On `pull_request`, the released `v0.5.2` Action can omit `base`: ProofDiff auto-resolves the exact `pull_request.base.sha` from GitHub's event payload. An explicit `base` always wins. If PR metadata is missing or malformed, the Action fails with an actionable error instead of silently falling back to an empty clean-working-tree diff. Other non-PR events preserve the historical working-tree fallback when `base` is omitted.
+On `pull_request`, the released `v0.5.3` Action can omit `base`: ProofDiff auto-resolves the exact `pull_request.base.sha` from GitHub's event payload. An explicit `base` always wins. If PR metadata is missing or malformed, the Action fails with an actionable error instead of silently falling back to an empty clean-working-tree diff. Other non-PR events preserve the historical working-tree fallback when `base` is omitted.
 
 Omitted `base` on `pull_request_target` fails closed instead of auto-resolving. GitHub's default checkout for `pull_request_target` normally points at the base repository revision, so combining that checkout with the PR base could misleadingly produce a zero diff. Prefer `pull_request` for untrusted changes. If you intentionally use `pull_request_target`, explicitly check out the trusted revision you intend to analyze and set `base` yourself.
 
 ## Declared source-to-test relationships
 
-The released `v0.5.2` Action exposes a `test-map` input corresponding to CLI `--test-map`.
+The released `v0.5.3` Action exposes a `test-map` input corresponding to CLI `--test-map`.
 
 ```yaml
-      - uses: hzw0813/proofdiff@v0.5.2
+      - uses: hzw0813/proofdiff@v0.5.3
         with:
           test-map: proofdiff.test-map.json
           run-checks: true
@@ -52,7 +52,7 @@ ProofDiff validates bounded map structure, exact test-path visibility, and snaps
 
 ## Immutable diff workspace binding
 
-The released `v0.5.2` Action deliberately fails closed when an immutable Git selection would otherwise be analyzed against a different checked-out filesystem state. For `base`/`range`, the selected target commit must be the checked-out `HEAD` and tracked worktree content must match it. For `staged`, tracked worktree content must match the index. Historical `A..B` analysis where `B` is not checked out should run from a checkout or separate worktree at `B`.
+The released `v0.5.3` Action deliberately fails closed when an immutable Git selection would otherwise be analyzed against a different checked-out filesystem state. For `base`/`range`, the selected target commit must be the checked-out `HEAD` and tracked worktree content must match it. For `staged`, tracked worktree content must match the index. Historical `A..B` analysis where `B` is not checked out should run from a checkout or separate worktree at `B`.
 
 Git-visible untracked files outside the immutable selection are rejected. Static-only analysis also rejects ignored root metadata and Python test-like files that current check discovery would read. When `run-checks: true`, ignored repository-local runtime inputs are rejected more broadly because repository-defined commands can consume them; bounded dependency/cache directories such as `node_modules` and virtual environments remain execution environment rather than declaration provenance.
 
@@ -62,7 +62,7 @@ The released Action writes a **ProofDiff · Change Evidence** job summary by def
 
 The summary is intentionally concise. Keep the upload step to retain the self-contained HTML report with full evidence, qualifications, observations, limitations, evidence-boundary detail, and bounded check output. The artifact step uses `if: always()` so a genuine verification failure does not hide its report.
 
-Use the released `v0.5.2` tag for normal stable integration. For an immutable security-sensitive pin, replace the tag with release snapshot `d2927b13aedb64403bdf1d6b3fe70f1148d1dce6`.
+Use the released `v0.5.3` tag for normal stable integration. For an immutable security-sensitive pin, replace the tag with release snapshot `d5fe3da78400a1b4d4154c0ddd9b84c3ef662e06`.
 
 The default is static-only and does not execute repository code. Set `run-checks: true` only in a job isolated from secrets and after accepting the repository-code execution risk described in [SECURITY.md](../SECURITY.md). Avoid `pull_request_target` for untrusted code. A **Related test file passed** result records a runner-qualified exact related target with at least one non-skipped passing test observation; relationship provenance can be inferred or explicitly declared, but neither shows that changed symbols or lines ran and neither is proof of correctness.
 
diff --git a/docs/troubleshooting.md b/docs/troubleshooting.md
index a7236e9..7fab5e9 100644
--- a/docs/troubleshooting.md
+++ b/docs/troubleshooting.md
@@ -26,7 +26,7 @@ For `--base`, fetch enough history for Git to find a merge base. For `--range`,
 
 ## Immutable base/range/staged analysis is rejected for workspace drift
 
-This is a fail-closed provenance check, not a verification failure. ProofDiff currently reads graph/config/test inputs from the checked-out filesystem, so v0.5.2 refuses to combine an immutable diff with another filesystem state. For `--base` and `--range`, make sure the selected target is the checked-out `HEAD` and the tracked worktree is clean relative to it. For `--staged`, make sure there are no unstaged tracked changes so the worktree matches the index. To inspect a historical `A..B` range, check out `B` or create a separate worktree at `B` first.
+This is a fail-closed provenance check, not a verification failure. ProofDiff currently reads graph/config/test inputs from the checked-out filesystem, so v0.5.3 refuses to combine an immutable diff with another filesystem state. For `--base` and `--range`, make sure the selected target is the checked-out `HEAD` and the tracked worktree is clean relative to it. For `--staged`, make sure there are no unstaged tracked changes so the worktree matches the index. To inspect a historical `A..B` range, check out `B` or create a separate worktree at `B` first.
 
 Git-visible untracked files are also outside an immutable selection. Commit, stage where appropriate, remove, ignore, or isolate them. Static-only analysis additionally rejects ignored metadata/Python tests that check discovery would consume. With `--run-checks`, ignored repository-local inputs are rejected more broadly because repository commands could read them; dependency/cache directories such as `node_modules` and virtual environments remain allowed environment inputs.