Add Kani formal-verification proofs for the finance programs (+ two program hardenings)

.claude/hooks/session-start.sh

@@ -0,0 +1,29 @@
+#!/bin/bash
+# SessionStart hook: install the Kani model checker so the formal-verification
+# proof crates (finance/escrow/kani-proofs, finance/token-swap/kani-proofs, ...)
+# can be run with `cargo kani` in Claude Code on the web.
+#
+# Synchronous + idempotent. The Kani toolchain (verifier + CBMC) is large, so
+# the first remote session pays the install cost; the container state is cached
+# afterwards, making subsequent sessions fast.
+set -euo pipefail
+
+# Only needed in the remote (web) environment; local machines manage their own
+# toolchains.
+if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
+  exit 0
+fi
+
+# Idempotent: nothing to do if Kani is already installed (e.g. cached container).
+if command -v cargo-kani >/dev/null 2>&1 && cargo kani --version >/dev/null 2>&1; then
+  echo "Kani already installed: $(cargo kani --version)"
+  exit 0
+fi
+
+echo "Installing kani-verifier..."
+cargo install --locked kani-verifier
+
+echo "Running kani setup (downloads the CBMC toolchain)..."
+kani setup
+
+echo "Kani ready: $(cargo kani --version)"

.claude/settings.json

@@ -0,0 +1,14 @@
+{
+  "hooks": {
+    "SessionStart": [
+      {
+        "hooks": [
+          {
+            "type": "command",
+            "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
+          }
+        ]
+      }
+    ]
+  }
+}

.github/workflows/kani.yml

@@ -0,0 +1,94 @@
+name: Kani
+
+# Formal-verification proofs (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.
+#
+# WHY THIS RUNS ON A WEEKLY SCHEDULE, NOT ON EVERY PUSH/PR
+# -------------------------------------------------------
+# Most of the finance proofs verify 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
+# 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).
+    - cron: "0 6 * * 1"
+  workflow_dispatch: {}
+  # Fast feedback only: the unit-test job below is gated to these events; the
+  # slow `verify` job is gated to schedule / manual dispatch.
+  push:
+    branches:
+      - main
+  pull_request:
+    types: [opened, synchronize, reopened]
+    branches:
+      - main
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+env:
+  # See https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
+  FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true
+
+jobs:
+  # Fast feedback on every push/PR: the proof 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.
+  unit-tests:
+    name: Proof unit tests (${{ matrix.program }})
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        program:
+          - escrow
+          - token-swap
+          - order-book
+          - lending
+          - betting-market
+          - vault-strategy
+          - token-fundraiser
+    steps:
+      - uses: actions/checkout@v5
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Run unit tests
+        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.
+  verify:
+    name: Kani proofs (${{ matrix.program }})
+    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        program:
+          - escrow
+          - token-swap
+          - order-book
+          - lending
+          - betting-market
+          - vault-strategy
+          - token-fundraiser
+    steps:
+      - uses: actions/checkout@v5
+      - name: Run Kani
+        uses: model-checking/kani-github-action@v1
+        with:
+          working-directory: finance/${{ matrix.program }}/kani-proofs

.gitignore

@@ -31,3 +31,7 @@ finance/escrow/native/tests/fixtures/escrow_native_program.so
 deploy
 .claude/*
 !.claude/skills/
+# Track the SessionStart hook (installs Kani) so Claude Code on the web can run
+# the formal-verification proof crates in future sessions.
+!.claude/settings.json
+!.claude/hooks/

README.md

@@ -29,6 +29,8 @@ To deploy to mainnet or devnet you'll need an RPC endpoint. [Quicknode](https://
 
 The programs below implement the core primitives of Solana DeFi: peer-to-peer trading (escrow), decentralized exchanges (AMM and order book), fundraising, yield-bearing vaults, and prediction markets. These are the building blocks used by protocols like Raydium, Orca, Openbook, and Kamino.
 
+> **Formal verification.** Every finance program ships with [Kani](https://github.com/model-checking/kani) formal-verification proofs (in `finance/<program>/kani-proofs/`), in the spirit of [aeyakovenko/percolator](https://github.com/aeyakovenko/percolator). The model checker proves each program's money-math invariants — value conservation, the AMM constant product, matching conservation, lending rounding/interest/liquidation safety, pari-mutuel solvency, share-vault solvency — exhaustively over all inputs, rather than just sampling them with unit tests. Most proofs verify nonlinear 128-bit arithmetic and are slow, so the full Kani run is [scheduled weekly](./.github/workflows/kani.yml) rather than gating every push. The proofs surfaced two (non-exploitable) edge cases — a lamport-write ordering in the native escrow and a zero-reserve drain in the AMM swap — both now hardened in the programs. See each crate's `README.md` for the harnesses, invariants, and findings.
+
 ### Escrow
 
 **Start here - the best first finance program to learn on Solana.** A neutral account that holds funds until both sides deliver, like a real-estate escrow or a lawyer's trust account. The maker deposits token A and names how much token B they want; when a taker supplies token B, the program swaps both in a single all-or-nothing transaction. This swap is the core idea behind every onchain exchange.

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

@@ -0,0 +1,21 @@
+# 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
+# conservation without the Solana / SPL-token CPI machinery, which Kani cannot
+# symbolically execute.
+[workspace]
+
+[package]
+name = "betting-market-kani-proofs"
+version = "0.1.0"
+edition = "2021"
+publish = false
+
+[lib]
+path = "src/lib.rs"
+
+[lints.rust]
+unexpected_cfgs = { level = "allow", check-cfg = ['cfg(kani)'] }
+
+[dependencies]

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

@@ -0,0 +1,56 @@
+# Betting-market — Kani proofs
+
+Formal-verification harnesses for 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.
+
+## What is verified
+
+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:
+
+| Harness | Property |
+| --- | --- |
+| `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). |
+| `proof_parimutuel_solvency` | **Solvency** (centrepiece): the winners collectively never claim more than the vault holds after the fee (`Σ payout_i <= winning_pool + distributable`). |
+| `proof_refund_conserves_pool` | On cancellation, refunds sum back to the total pool — neither over- nor under-drained. |
+
+### The solvency proof
+
+After settlement the vault holds `winning_pool + distributable_losing_pool`.
+Each winner is paid `stake_i + floor(stake_i · D / winning_pool)`, and the
+winning stakes sum to `winning_pool`. Because
+`Σ floor(stake_i·D/W) <= Σ stake_i·D/W = D`, total payouts are
+`<= winning_pool + D` — exactly the vault balance. So no set of winners can drain
+the vault below zero; floor rounding only ever leaves dust behind. Modelled with
+3 winners whose stakes sum to the winning pool.
+
+## Bounded model checking
+
+The settlement, payout, and solvency proofs verify 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
+the number of bettors).
+
+| Harness | Bound | Time |
+| --- | --- | --- |
+| `proof_settlement_fee_and_split` | `total_pool <= 4095`, `fee_bps` symbolic | ~1s |
+| `proof_winner_never_below_stake` | `winning_pool/distributable <= 255` | ~6s |
+| `proof_parimutuel_solvency` | 3 winners, stakes `<= 7`, `distributable <= 63` | ~3s |
+| `proof_refund_conserves_pool` | 4 bettors, full `u64` | <1s |
+
+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.
+
+## Running
+
+```bash
+cargo test                                                 # unit tests, no Kani
+cargo install --locked kani-verifier && cargo kani setup   # one-time
+cargo kani                                                  # formal verification
+```