Call the Kani harnesses model checks, not proofs

.github/workflows/kani.yml

@@ -1,27 +1,30 @@
 name: Kani
 
-# Formal-verification proofs (https://github.com/model-checking/kani) for the
+# Kani model checks (https://github.com/model-checking/kani) for the
 # finance/ example programs. Each <program>/kani-proofs crate models its
-# program's pure money-math and lets the Kani model checker prove the invariants
-# exhaustively, in the spirit of aeyakovenko/percolator.
+# program's pure arithmetic and lets the Kani model checker check the invariants
+# exhaustively over each harness's declared inputs, in the spirit of
+# aeyakovenko/percolator. Kani marks a harness with #[kani::proof], which is why
+# the crates are named kani-proofs and the harnesses proof_*; each one is a
+# model check.
 #
 # WHY THIS RUNS ON A WEEKLY SCHEDULE, NOT ON EVERY PUSH/PR
 # -------------------------------------------------------
-# Most of the finance proofs verify NONLINEAR 128-bit arithmetic (constant-
+# Most of the finance harnesses check NONLINEAR 128-bit arithmetic (constant-
 # product curves, mul_div with a symbolic divisor, integer sqrt, pari-mutuel
 # payouts, share exchange rates). Kani is a bit-precise model checker: it
 # bit-blasts that arithmetic into SAT, and nonlinear / symbolic-divisor terms
 # are the worst case for the solver. Even with bounded inputs, individual
 # harnesses take tens of seconds and a full crate runs for minutes; the whole
 # finance suite is far too slow to gate every push/PR. So the heavy
-# `cargo kani` verification runs once a week (and on demand via
+# `cargo kani` model check runs once a week (and on demand via
 # workflow_dispatch), while a fast unit-test job still runs on every push/PR to
 # catch model regressions early. See each finance/<program>/kani-proofs/README.md
 # for the per-harness bounds and timings.
 
 on:
   schedule:
-    # Mondays at 06:00 UTC. Weekly because the proofs are slow (see header).
+    # Mondays at 06:00 UTC. Weekly because the model checks are slow (see header).
     - cron: "0 6 * * 1"
   workflow_dispatch: {}
   # Fast feedback only: the unit-test job below is gated to these events; the
@@ -43,9 +46,9 @@ env:
   FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true
 
 jobs:
-  # Fast feedback on every push/PR: the proof crates compile and their plain
+  # Fast feedback on every push/PR: the Kani crates compile and their plain
   # unit tests pass on stable, independently of the (slow) Kani toolchain. This
-  # catches model regressions without paying for full verification.
+  # catches model regressions without paying for the full model check.
   unit-tests:
     name: Proof unit tests (${{ matrix.program }})
     runs-on: ubuntu-latest
@@ -67,7 +70,7 @@ jobs:
       - uses: dtolnay/rust-toolchain@stable
         with:
           components: rustfmt, clippy
-      # Each proof crate declares its own `[workspace]`, so the repository-wide
+      # Each Kani crate declares its own `[workspace]`, so the repository-wide
       # `cargo fmt` and `cargo clippy` jobs in rust.yml never see it. Lint here
       # instead, or these crates drift.
       - name: Enforce formatting
@@ -80,15 +83,15 @@ jobs:
         working-directory: finance/${{ matrix.program }}/kani-proofs
         run: cargo test
 
-  # The formal verification itself. SLOW (minutes per crate), so it only runs on
-  # the weekly schedule or when triggered manually — never on push/PR. The
-  # official Kani action installs the verifier + CBMC toolchain (with caching)
-  # and runs `cargo kani` in each proof crate; any failed proof fails the job.
+  # The model check itself. SLOW (minutes per crate), so it only runs on the
+  # weekly schedule or when triggered manually, never on push/PR. The official
+  # Kani action installs the model checker + CBMC toolchain (with caching) and
+  # runs `cargo kani` in each Kani crate; any failed harness fails the job.
   verify:
     name: Kani proofs (${{ matrix.program }})
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
-    # Every crate's proofs complete in under ~3 minutes. A harness whose bounds
+    # Every crate's harnesses complete in under ~3 minutes. A harness whose bounds
     # make the solver blow up otherwise runs into the runner's 6-hour hard
     # limit and surfaces as an easy-to-miss "cancelled" run (this happened:
     # prop-amm's quote-bracketing harness with an unbounded u64 price). Fail

README.md

@@ -32,7 +32,7 @@ To deploy to mainnet or devnet you'll need an RPC endpoint. [Quicknode](https://
 
 ## Financial software ("DeFi")
 
-The programs are examples of common financial primitives on Solana. As well as tests these all have [formal verification using Kani](https://github.com/model-checking/kani). Every finance program ships with proofs that verify its money-math invariants exhaustively over all inputs. See each program's `kani-proofs/` directory for the harnesses and what they prove.
+The programs are examples of common financial primitives on Solana. As well as tests these all have [Kani](https://github.com/model-checking/kani) model checks. Every finance program ships with Kani harnesses that check its arithmetic invariants exhaustively over the inputs each harness declares. Kani marks a harness with `#[kani::proof]`, which is why each program's directory is `kani-proofs/` and the harnesses are named `proof_*`; each one is a model check. See each program's `kani-proofs/` directory for the harnesses and what they check.
 
 ### Escrow
 
@@ -427,7 +427,7 @@ Work through the [finance examples](#financial-software-defi) in order of comple
 
 ### Are these examples production-ready?
 
-They are teaching examples: every one builds and passes CI, and the finance programs additionally carry [Kani](https://github.com/model-checking/kani) formal-verification proofs of their money math. None are audited or deployed to mainnet, so treat them as reference implementations to learn from, not code to deploy as-is.
+They are teaching examples: every one builds and passes CI, and the finance programs additionally carry [Kani](https://github.com/model-checking/kani) model checks of their arithmetic. None are audited or deployed to mainnet, so treat them as reference implementations to learn from, not code to deploy as-is.
 
 ## Acknowledgements
 

finance/betting-market/kani-proofs/Cargo.toml

@@ -1,7 +1,7 @@
 # Standalone workspace - intentionally NOT part of the root program-examples
 # workspace. Kani (https://github.com/model-checking/kani) proof harnesses that
 # model the betting market's pari-mutuel payout math (settlement fee/split and
-# the pro-rata winner payout) so the model checker can verify solvency and
+# the pro-rata winner payout) so the model checker can check solvency and
 # conservation without the Solana / SPL-token CPI machinery, which Kani cannot
 # symbolically execute.
 [workspace]

finance/betting-market/kani-proofs/README.md

@@ -1,16 +1,20 @@
-# Betting-market: Kani proofs
+# Betting-market: Kani model checks
 
-Formal-verification harnesses for the pari-mutuel betting market, in the spirit
+Kani harnesses that model-check the pari-mutuel betting market, in the spirit
 of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which
-uses the [Kani](https://github.com/model-checking/kani) model checker to prove
-the mathematical correctness of a DeFi engine.
+uses the [Kani](https://github.com/model-checking/kani) model checker to check
+the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`,
+which is why the crate is `kani-proofs` and the harnesses are named `proof_*`;
+each one is a model check: Kani tries every value of the inputs the harness
+declares and reports either that every assertion held or an input that breaks
+one.
 
-## What is verified
+## What is checked
 
 Every stake lands in one vault; at settlement the losing pool (minus a fee) is
 split among the winners in proportion to their stake. The token movement goes
 through SPL CPIs Kani cannot symbolically execute, but the payout math is pure
-integer arithmetic. This crate reproduces it faithfully and proves:
+integer arithmetic. This crate reproduces it faithfully and checks, for every input:
 
 - `proof_settlement_fee_and_split`: `fee <= losing_pool` (so `distributable` never underflows) and `winning + distributable + fee == total`, settlement conserves the pool.
 - `proof_winner_never_below_stake`: `payout = stake + winnings >= stake`: a winner is never paid less than they staked (the fee is charged only on losers).
@@ -19,7 +23,7 @@ integer arithmetic. This crate reproduces it faithfully and proves:
 - `proof_betting_and_settlement_windows_partition_time`: at every instant exactly one of `betting_is_open` and `may_settle` holds, so no bet can land once the event can be settled.
 - `proof_outcomes_fixed_before_money_arrives`: a model of the event's lifecycle guards (`add_outcome`, `open_betting`, `place_bet`, `settle_event`, `cancel_event`), run over every sequence of six calls at arbitrary times from a fresh draft. The outcome list never changes once money is in the pool, every stake lands in a market with at least two outcomes and before the close time, and settlement happens only at or after it.
 
-### The solvency proof
+### The solvency check
 
 After settlement the vault holds `winning_pool + distributable_losing_pool`.
 Each winner is paid `stake_i + floor(stake_i · D / winning_pool)`, and the
@@ -31,11 +35,11 @@ the vault below zero; floor rounding only ever leaves dust behind. Modelled with
 
 ## Bounded model checking
 
-The settlement, payout, and solvency proofs verify nonlinear 128-bit arithmetic
+The settlement, payout, and solvency harnesses check nonlinear 128-bit arithmetic
 (`stake · distributable`, divided by the symbolic winning pool), the hard case
 for a bit-precise solver, so (as percolator does) they bound their symbolic
 inputs to a representative range; the pro-rata identity is scale-invariant. The
-refund proof is pure linear logic and runs at full `u64` width (bounded only in
+refund harness is pure linear logic and runs at full `u64` width (bounded only in
 the number of bettors).
 
 - `proof_settlement_fee_and_split`: `total_pool <= 4095`, `fee_bps` symbolic, ~1s
@@ -45,12 +49,12 @@ the number of bettors).
 - `proof_betting_and_settlement_windows_partition_time`: full `i64`, <1s
 - `proof_outcomes_fixed_before_money_arrives`: 6 calls, full `u64` stakes and `i64` times, ~2s
 
-Run weekly in CI (the `.github/workflows/kani.yml` `verify` job), not on every push/PR, because the bounded nonlinear proofs are slow. A fast unit-test job runs per push/PR.
+Run weekly in CI (the `.github/workflows/kani.yml` `verify` job), not on every push/PR, because the bounded nonlinear model checks are slow. A fast unit-test job runs per push/PR.
 
 ## Running
 
 ```bash
 cargo test                                                 # unit tests, no Kani
 cargo install --locked kani-verifier && cargo kani setup   # one-time
-cargo kani                                                  # formal verification
+cargo kani                                                  # Kani model checks
 ```

finance/betting-market/kani-proofs/src/lib.rs

@@ -1,17 +1,20 @@
-//! Kani proof harnesses for the betting-market program (`finance/betting-market`).
+//! Kani harnesses for the betting-market program (`finance/betting-market`).
 //!
 //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to
-//! prove the mathematical correctness of a DeFi engine's pure numeric core.
+//! check the arithmetic of a DeFi engine's pure numeric core. Kani marks a
+//! harness with `#[kani::proof]`, which is why the crate is `kani-proofs` and
+//! the harnesses are named `proof_*`; each one is a model check over every value
+//! of the inputs it declares.
 //!
 //! The program is a pari-mutuel betting market: every stake lands in one vault,
 //! and at settlement the losing pool (minus a fee) is split among the winners in
 //! proportion to their stake. The token movement goes through SPL CPIs Kani
 //! cannot symbolically execute, but the payout math (`settle_event`,
 //! `claim_winnings`) is pure integer arithmetic. This crate reproduces it
-//! faithfully and proves the two properties that matter: **solvency** (winners
+//! faithfully and checks the two properties that matter: **solvency** (winners
 //! can never collectively claim more than the vault holds) and that a winner is
 //! never paid less than their own stake. A small model of the event's
-//! lifecycle guards also proves the outcome list is fixed before any money
+//! lifecycle guards also checks that the outcome list is fixed before any money
 //! arrives and that the betting and settlement windows never overlap.
 //!
 //! The nonlinear harness uses bounded model checking (small symbolic inputs), as

finance/escrow/anchor-v1/README.md

@@ -61,9 +61,9 @@ Yes. Escrow is the smallest complete finance program: one state PDA, one vault,
 
 Build with `anchor build`, then run `cargo test`. The tests are Rust integration tests against [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm), so no local validator is needed.
 
-### How is this escrow program verified?
+### How is this escrow program tested?
 
-Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/) that check the money-math invariants over all possible inputs, not just test cases.
+Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/) that check the arithmetic invariants for every input in their declared ranges, not just test cases.
 
 ## Credit
 

finance/escrow/anchor/README.md

@@ -61,9 +61,9 @@ Yes. Escrow is the smallest complete finance program: one state PDA, one vault,
 
 Build with `anchor build`, then run `cargo test`. The tests are Rust integration tests against [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm), so no local validator is needed.
 
-### How is this escrow program verified?
+### How is this escrow program tested?
 
-Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/) that check the money-math invariants over all possible inputs, not just test cases.
+Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/) that check the arithmetic invariants for every input in their declared ranges, not just test cases.
 
 ## Credit
 

finance/escrow/kani-proofs/README.md

@@ -1,18 +1,23 @@
-# Escrow: Kani proofs
+# Escrow: Kani model checks
 
-Formal-verification harnesses for the escrow program, in the spirit of
+Kani model-check harnesses for the escrow program, in the spirit of
 [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which
-uses the [Kani](https://github.com/model-checking/kani) model checker to prove
-the mathematical correctness of a DeFi engine.
+uses the [Kani](https://github.com/model-checking/kani) model checker to check
+the arithmetic of a DeFi engine.
 
-## What is verified
+Kani marks a harness with `#[kani::proof]`, which is why the crate is
+`kani-proofs` and the harnesses are named `proof_*`; each one is a model check:
+it tries every value of its declared inputs and reports either that every
+assertion held or the input that breaks one.
+
+## What is checked
 
 The escrow program itself does almost no arithmetic, it delegates token
 movement to the SPL token program through CPIs, which Kani cannot symbolically
-execute. So (exactly like percolator, which verifies a self-contained library)
-this crate models the escrow's *verifiable core* as pure Rust functions that
-mirror the on-chain code's arithmetic and statement ordering, and proves the
-invariants the program relies on:
+execute. So (exactly like percolator, which model-checks a self-contained
+library) this crate models the escrow's *checkable core* as pure Rust functions
+that mirror the on-chain code's arithmetic and statement ordering, and checks
+the invariants the program relies on:
 
 - `proof_token_transfer_conserves`: An SPL transfer either fails atomically or conserves the two accounts' total balance.
 - `proof_close_offer_conserves_on_success`: Closing the offer account conserves lamports and empties the source.
@@ -54,16 +59,16 @@ let new_destination_lamports = destination_lamports
 **offer_info.lamports.borrow_mut() = 0;
 ```
 
-`proof_close_offer_conserves_lamports_unconditionally` now proves lamport
+`proof_close_offer_conserves_lamports_unconditionally` now checks that lamport
 conservation holds with **equality on every path**, with no precondition, the
 invariant no longer depends on the runtime reverting a failed instruction. (This
-is also why it's a plain proof, not a `#[kani::should_panic]`: a should-panic
+is also why it's a plain harness, not a `#[kani::should_panic]`: a should-panic
 encoding would have *started failing* the moment this fix landed.)
 
 ## CI
 
-These proofs run **weekly** (and on demand) in the `.github/workflows/kani.yml`
-`verify` job, alongside the other `finance/` proof crates, the nonlinear ones
+These model checks run **weekly** (and on demand) in the `.github/workflows/kani.yml`
+`verify` job, alongside the other `finance/` Kani crates, the nonlinear ones
 are slow, so the full Kani run is scheduled rather than gating every push/PR. A
 fast `cargo test` job runs per push/PR to catch model regressions early.
 
@@ -73,7 +78,7 @@ fast `cargo test` job runs per push/PR to catch model regressions early.
 # Plain unit tests (no Kani required):
 cargo test
 
-# Formal verification (requires Kani):
+# Kani model checks (requires Kani):
 cargo install --locked kani-verifier && cargo kani setup   # one-time
 cargo kani
 ```