Skip to content

Commit 2c4ea7e

Browse files
mikemaccanamikemaccana
authored
Merge branch 'main' into claude/quicknode-solana-programs-plsus8
2 parents a10e5b1 + dd7ea71 commit 2c4ea7e

30 files changed

Lines changed: 2794 additions & 4 deletions

File tree

‎.claude/hooks/session-start.sh‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#!/bin/bash
2+
# SessionStart hook: install the Kani model checker so the formal-verification
3+
# proof crates (finance/escrow/kani-proofs, finance/token-swap/kani-proofs, ...)
4+
# can be run with `cargo kani` in Claude Code on the web.
5+
#
6+
# Synchronous + idempotent. The Kani toolchain (verifier + CBMC) is large, so
7+
# the first remote session pays the install cost; the container state is cached
8+
# afterwards, making subsequent sessions fast.
9+
set -euo pipefail
10+
11+
# Only needed in the remote (web) environment; local machines manage their own
12+
# toolchains.
13+
if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
14+
exit 0
15+
fi
16+
17+
# Idempotent: nothing to do if Kani is already installed (e.g. cached container).
18+
if command -v cargo-kani >/dev/null 2>&1 && cargo kani --version >/dev/null 2>&1; then
19+
echo "Kani already installed: $(cargo kani --version)"
20+
exit 0
21+
fi
22+
23+
echo "Installing kani-verifier..."
24+
cargo install --locked kani-verifier
25+
26+
echo "Running kani setup (downloads the CBMC toolchain)..."
27+
kani setup
28+
29+
echo "Kani ready: $(cargo kani --version)"

‎.claude/settings.json‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
{
2+
"hooks": {
3+
"SessionStart": [
4+
{
5+
"hooks": [
6+
{
7+
"type": "command",
8+
"command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
9+
}
10+
]
11+
}
12+
]
13+
}
14+
}

‎.github/workflows/kani.yml‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
name: Kani
2+
3+
# Formal-verification proofs (https://github.com/model-checking/kani) for the
4+
# finance/ example programs. Each <program>/kani-proofs crate models its
5+
# program's pure money-math and lets the Kani model checker prove the invariants
6+
# exhaustively, in the spirit of aeyakovenko/percolator.
7+
#
8+
# WHY THIS RUNS ON A WEEKLY SCHEDULE, NOT ON EVERY PUSH/PR
9+
# -------------------------------------------------------
10+
# Most of the finance proofs verify NONLINEAR 128-bit arithmetic (constant-
11+
# product curves, mul_div with a symbolic divisor, integer sqrt, pari-mutuel
12+
# payouts, share exchange rates). Kani is a bit-precise model checker: it
13+
# bit-blasts that arithmetic into SAT, and nonlinear / symbolic-divisor terms
14+
# are the worst case for the solver. Even with bounded inputs, individual
15+
# harnesses take tens of seconds and a full crate runs for minutes; the whole
16+
# finance suite is far too slow to gate every push/PR. So the heavy
17+
# `cargo kani` verification runs once a week (and on demand via
18+
# workflow_dispatch), while a fast unit-test job still runs on every push/PR to
19+
# catch model regressions early. See each finance/<program>/kani-proofs/README.md
20+
# for the per-harness bounds and timings.
21+
22+
on:
23+
schedule:
24+
# Mondays at 06:00 UTC. Weekly because the proofs are slow (see header).
25+
- cron: "0 6 * * 1"
26+
workflow_dispatch: {}
27+
# Fast feedback only: the unit-test job below is gated to these events; the
28+
# slow `verify` job is gated to schedule / manual dispatch.
29+
push:
30+
branches:
31+
- main
32+
pull_request:
33+
types: [opened, synchronize, reopened]
34+
branches:
35+
- main
36+
37+
concurrency:
38+
group: ${{ github.workflow }}-${{ github.ref }}
39+
cancel-in-progress: true
40+
41+
env:
42+
# See https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
43+
FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true
44+
45+
jobs:
46+
# Fast feedback on every push/PR: the proof crates compile and their plain
47+
# unit tests pass on stable, independently of the (slow) Kani toolchain. This
48+
# catches model regressions without paying for full verification.
49+
unit-tests:
50+
name: Proof unit tests (${{ matrix.program }})
51+
runs-on: ubuntu-latest
52+
strategy:
53+
fail-fast: false
54+
matrix:
55+
program:
56+
- escrow
57+
- token-swap
58+
- order-book
59+
- lending
60+
- betting-market
61+
- vault-strategy
62+
- token-fundraiser
63+
steps:
64+
- uses: actions/checkout@v5
65+
- uses: dtolnay/rust-toolchain@stable
66+
- name: Run unit tests
67+
working-directory: finance/${{ matrix.program }}/kani-proofs
68+
run: cargo test
69+
70+
# The formal verification itself. SLOW (minutes per crate), so it only runs on
71+
# the weekly schedule or when triggered manually — never on push/PR. The
72+
# official Kani action installs the verifier + CBMC toolchain (with caching)
73+
# and runs `cargo kani` in each proof crate; any failed proof fails the job.
74+
verify:
75+
name: Kani proofs (${{ matrix.program }})
76+
if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
77+
runs-on: ubuntu-latest
78+
strategy:
79+
fail-fast: false
80+
matrix:
81+
program:
82+
- escrow
83+
- token-swap
84+
- order-book
85+
- lending
86+
- betting-market
87+
- vault-strategy
88+
- token-fundraiser
89+
steps:
90+
- uses: actions/checkout@v5
91+
- name: Run Kani
92+
uses: model-checking/kani-github-action@v1
93+
with:
94+
working-directory: finance/${{ matrix.program }}/kani-proofs

‎.github/workflows/solana-asm.yml‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -199,8 +199,17 @@ jobs:
199199
# Make the script executable
200200
chmod +x build_and_test.sh
201201
202-
# Install sbpf assembler
203-
cargo install --git https://github.com/blueshift-gg/sbpf.git
202+
# Install sbpf assembler.
203+
#
204+
# Pin to a specific revision: installing from the branch HEAD makes the
205+
# build non-reproducible and breaks CI whenever sbpf changes its output.
206+
# On 2026-06-29 sbpf merged its SBPF v3 work (PR #127), switching the
207+
# emitted ELF to the v3 / 0x03 OS-ABI format. litesvm 0.11.0's loader
208+
# rejects that format, so every asm test started failing at
209+
# `svm.add_program(...).unwrap()` with Instruction(InvalidAccountData).
210+
# This rev is the last commit before the v3 changes and matches the
211+
# toolchain from the last green run; bump it together with litesvm.
212+
cargo install --git https://github.com/blueshift-gg/sbpf.git --rev 0223df0e7ba622d4956b4ecf3cf2397f6945b76b
204213
- name: Setup Solana Stable
205214
uses: heyAyushh/setup-solana@v5.9
206215
with:

‎.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,7 @@ finance/escrow/native/tests/fixtures/escrow_native_program.so
3131
deploy
3232
.claude/*
3333
!.claude/skills/
34+
# Track the SessionStart hook (installs Kani) so Claude Code on the web can run
35+
# the formal-verification proof crates in future sessions.
36+
!.claude/settings.json
37+
!.claude/hooks/

‎README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ To deploy to mainnet or devnet you'll need an RPC endpoint. [Quicknode](https://
2929

3030
The programs are examples of common financial primitives on Solana.
3131

32+
> **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.
33+
3234
### Escrow
3335

3436
**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‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
# Standalone workspace - intentionally NOT part of the root program-examples
2+
# workspace. Kani (https://github.com/model-checking/kani) proof harnesses that
3+
# model the betting market's pari-mutuel payout math (settlement fee/split and
4+
# the pro-rata winner payout) so the model checker can verify solvency and
5+
# conservation without the Solana / SPL-token CPI machinery, which Kani cannot
6+
# symbolically execute.
7+
[workspace]
8+
9+
[package]
10+
name = "betting-market-kani-proofs"
11+
version = "0.1.0"
12+
edition = "2021"
13+
publish = false
14+
15+
[lib]
16+
path = "src/lib.rs"
17+
18+
[lints.rust]
19+
unexpected_cfgs = { level = "allow", check-cfg = ['cfg(kani)'] }
20+
21+
[dependencies]

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

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# Betting-market — Kani proofs
2+
3+
Formal-verification harnesses for the pari-mutuel betting market, in the spirit
4+
of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which
5+
uses the [Kani](https://github.com/model-checking/kani) model checker to prove
6+
the mathematical correctness of a DeFi engine.
7+
8+
## What is verified
9+
10+
Every stake lands in one vault; at settlement the losing pool (minus a fee) is
11+
split among the winners in proportion to their stake. The token movement goes
12+
through SPL CPIs Kani cannot symbolically execute, but the payout math is pure
13+
integer arithmetic. This crate reproduces it faithfully and proves:
14+
15+
| Harness | Property |
16+
| --- | --- |
17+
| `proof_settlement_fee_and_split` | `fee <= losing_pool` (so `distributable` never underflows) and `winning + distributable + fee == total` — settlement conserves the pool. |
18+
| `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+
| `proof_parimutuel_solvency` | **Solvency** (centrepiece): the winners collectively never claim more than the vault holds after the fee (`Σ payout_i <= winning_pool + distributable`). |
20+
| `proof_refund_conserves_pool` | On cancellation, refunds sum back to the total pool — neither over- nor under-drained. |
21+
22+
### The solvency proof
23+
24+
After settlement the vault holds `winning_pool + distributable_losing_pool`.
25+
Each winner is paid `stake_i + floor(stake_i · D / winning_pool)`, and the
26+
winning stakes sum to `winning_pool`. Because
27+
`Σ floor(stake_i·D/W) <= Σ stake_i·D/W = D`, total payouts are
28+
`<= winning_pool + D` — exactly the vault balance. So no set of winners can drain
29+
the vault below zero; floor rounding only ever leaves dust behind. Modelled with
30+
3 winners whose stakes sum to the winning pool.
31+
32+
## Bounded model checking
33+
34+
The settlement, payout, and solvency proofs verify nonlinear 128-bit arithmetic
35+
(`stake · distributable`, divided by the symbolic winning pool), the hard case
36+
for a bit-precise solver, so — as percolator does — they bound their symbolic
37+
inputs to a representative range; the pro-rata identity is scale-invariant. The
38+
refund proof is pure linear logic and runs at full `u64` width (bounded only in
39+
the number of bettors).
40+
41+
| Harness | Bound | Time |
42+
| --- | --- | --- |
43+
| `proof_settlement_fee_and_split` | `total_pool <= 4095`, `fee_bps` symbolic | ~1s |
44+
| `proof_winner_never_below_stake` | `winning_pool/distributable <= 255` | ~6s |
45+
| `proof_parimutuel_solvency` | 3 winners, stakes `<= 7`, `distributable <= 63` | ~3s |
46+
| `proof_refund_conserves_pool` | 4 bettors, full `u64` | <1s |
47+
48+
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.
49+
50+
## Running
51+
52+
```bash
53+
cargo test # unit tests, no Kani
54+
cargo install --locked kani-verifier && cargo kani setup # one-time
55+
cargo kani # formal verification
56+
```

0 commit comments

Comments
 (0)