Add Kani formal-verification proofs for the finance programs (+ two program hardenings)#85
Merged
Merged
Conversation
Model the escrow's value-conservation and lamport-accounting core as pure Rust and prove the invariants with the Kani model checker, in the spirit of aeyakovenko/percolator. The on-chain program delegates token movement to the SPL token program via CPIs that Kani cannot symbolically execute, so the harnesses faithfully reproduce the in-program arithmetic and statement ordering. 10 harnesses cover: SPL transfer conservation, take/cancel/make-offer value conservation, the (unreachable) checked_add conservation guards, and the PDA id-seed round-trip. Finding: utils::close_offer_account zeroes the source account before the fallible checked_add that credits the destination; at offer == dest == u64::MAX the credit overflows and returns Err after the zeroing, momentarily destroying lamports. Not exploitable (the runtime reverts on Err and a wallet cannot hold ~u64::MAX lamports). Captured as an expected-fail (#[kani::should_panic]) harness so CI stays green while the finding is documented. Wire escrow proofs into CI via a new Kani workflow (unit tests on stable + formal verification via the official kani-github-action). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
Extend the Kani proof harnesses (introduced for escrow) to the constant-product AMM. The on-chain instructions delegate token movement to the SPL token program via CPIs that Kani cannot symbolically execute, so the harnesses faithfully reproduce the pure arithmetic (same u128 widening, multiply-before-divide, floor rounding) and prove its invariants: - fee split: fee <= input, admin_portion <= fee, taxed_input + fee == input - constant product: a swap never decreases k = reserve_in * reserve_out - solvency: with a non-empty input reserve, output < other_reserve - integer_sqrt returns the exact floor: r^2 <= n < (r+1)^2 - withdraw never exceeds the reserve (MINIMUM_LIQUIDITY floor) - deposit ratio clamp never spends more than the caller offered Several harnesses verify nonlinear 128-bit arithmetic, the worst case for a bit-precise model checker, so they use bounded model checking (constraining symbolic inputs to a representative range) exactly as percolator does. They are intentionally NOT wired into CI yet (CI runs the fast, unbounded escrow proofs). Finding: when an input-side effective reserve is exactly 0, the curve outputs the entire opposite reserve, and the require!(new_invariant >= invariant) guard does not catch it (pre-trade k is already 0). Latent edge, not a live exploit (the deposit path's MINIMUM_LIQUIDITY floor prevents a zero reserve). Captured as an expected-fail (#[kani::should_panic]) harness. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
The nonlinear 128-bit harnesses needed per-harness input bounds to stay tractable for the bit-precise solver (bounded model checking, as percolator does). Sized each bound to its difficulty: integer_sqrt n<=255 with unwind(11) (symbolic 128-bit division per Newton iteration), constant-product reserves <=63, swap-solvency <=255, deposit ratio clamp <=31 (symbolic-by-symbolic division, the hardest), fee-split/withdraw <=4095. Whole suite now verifies in ~80s: 7 harnesses, 0 failures. Document the bounds and times in the README. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
SessionStart hook (.claude/hooks/session-start.sh, registered in .claude/settings.json) installs the Kani verifier + CBMC toolchain in Claude Code on the web so the formal-verification proof crates can run with `cargo kani`. Synchronous and idempotent (skips if Kani is already present, so cached containers start fast); guarded to the remote environment only. Whitelist .claude/settings.json and .claude/hooks/ in .gitignore so the hook is tracked. Extend the Kani proofs to the order-book program (finance/order-book/kani-proofs) with bounded model checking. 5 harnesses, all green: - matching conservation: total_filled + taker_remaining == incoming_quantity (so place_order's quantity.checked_sub(taker_remaining) never underflows) - matching respects price-crossing and never overfills a resting maker - ceiling fee fee = ceil(gross*bps/10000) is a true ceiling and <= gross, so gross - fee never underflows and the require!(fee <= gross) guard is dead code - bid price-improvement rebate locked - gross >= 0 never underflows (fills clear at the maker's better price) - order remaining + filled == original The matching/bookkeeping proofs run at full u64 width; the nonlinear fee/rebate proofs bound their inputs to stay tractable for the bit-precise solver, exactly as percolator does. Not wired into CI (slower, bounded); the escrow proofs gate CI. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
Extend the Kani proofs to the Solend-style lending program (the richest of the finance examples), with bounded model checking. 8 harnesses, all green: - mul_div_floor / mul_div_ceil are the true floor/ceil of a*b/d, differ by <=1, and coincide iff the division is exact - directional rounding is protocol-favourable: ceil >= floor, so debt is never undercounted and a supplier claim never overcounted (no dust extraction) - the cumulative borrow-rate index is monotonically non-decreasing (borrowers always owe >= principal) - utilization is always a valid [0, 10000] bps fraction - the kinked borrow-rate curve stays within [min_rate, max_rate] for every utilization, given the validated config ordering - a deposit->redeem round-trip never returns more liquidity than deposited (both legs floor) - no rounding drain of the pool - a liquidation never repays more than the debt (close factor <= 100%) - seized value always includes the bonus (liquidator never under-compensated) Several harnesses divide by a symbolic divisor (mul_div's d, the index scale, the rate curve's full-optimal), the hardest shape for the bit-precise solver, so they bound inputs tightly. Two make a normally-constant denominator a parameter (the index uses a small symbolic scale instead of FIXED_POINT_SCALE 10^18; the rate curve takes full_utilization instead of the constant 10000) so the scale-invariant property can be proven at a tractable scale. Not wired into CI (slower, bounded); the escrow proofs gate CI. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
Model the pari-mutuel payout math (settle_event, claim_winnings, claim_refund) and prove its invariants with bounded model checking. 4 harnesses, all green: - settlement conserves the pool: fee <= losing_pool (distributable never underflows) and winning + distributable + fee == total - a winner is never paid less than they staked (payout = stake + winnings) - solvency (centrepiece): winners collectively never claim more than the vault holds after the fee, because sum(floor(stake_i*D/W)) <= D when the winning stakes sum to W; modelled with 3 winners - on cancellation, refunds sum back to the total pool The nonlinear payout/solvency proofs bound their inputs (stake*distributable divided by the symbolic winning pool); the refund conservation proof runs at full u64 width. Not wired into CI (bounded); the escrow proofs gate CI. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
Complete the finance/ sweep: every finance program now has Kani proofs. vault-strategy (ERC4626-style share vault), 3 harnesses with bounded model checking: - withdrawal solvency: floor(balance*shares/total) <= balance (a withdrawal never overdraws any vault leg), and burning the whole supply takes exactly the whole balance - deposit->withdraw round-trip never returns more than deposited (no rounding attack mints shares worth more than they cost) - the time-based manager fee can never mint more than 100%/year of dilution token-fundraiser, 3 harnesses: - the per-contributor cap never exceeds the goal and bounds every cumulative total (nonlinear, bounded) - current_amount always equals the sum of contributions (linear, full u64) - refunds sum back to current_amount on a failed raise (linear, full u64) Not wired into CI (bounded/slower); the escrow proofs gate CI. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
…ve proofs CI: the formal proofs now cover all seven finance/ programs and run on a weekly schedule (plus manual workflow_dispatch), because most verify nonlinear 128-bit arithmetic and are slow (minutes per crate) - the workflow header documents this as the reason for the schedule. A fast unit-test job still runs per push/PR across all proof crates to catch model regressions early. Replace both #[kani::should_panic] "finding" harnesses with positive proofs. should_panic inverts the maintenance signal - fixing the underlying code would make a should-panic harness start failing - so it is the wrong tool for recording a known, non-exploitable edge: - escrow: proof_close_offer_never_creates_lamports proves the unconditional "no inflation" property (after <= before on every path); the transient lamport-destruction-on-overflow wart is documented in the harness comment - token-swap: proof_swap_at_zero_reserve_drains_whole_pool proves the edge as a true characterization (output == other_reserve and the k-guard passes 0 >= 0) Update the root README to note that every finance program ships Kani formal proofs (with the weekly-schedule rationale), and update each crate README to reflect the weekly CI run and the renamed harnesses. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
Rather than just documenting the two non-exploitable edges the proofs surfaced, fix them at the source - the better remedy - and strengthen the proofs to the now-unconditional invariants. escrow (native/program/src/utils.rs): close_offer_account used to zero the source account's lamports before the fallible checked_add that credits the destination, so an overflow returned Err after destroying the source's lamports (masked on-chain only by the runtime reverting failed instructions). Reorder to compute-then-commit: run the checked_add first, mutate nothing until it succeeds. Lamport conservation now holds with equality on every path from the function's own logic. proof_close_offer_conserves_lamports_unconditionally proves it with no precondition. token-swap (swap_tokens.rs): the constant-product curve drains the whole opposite reserve when an input-side effective reserve is 0, and the new_invariant >= invariant guard does not catch it (k = 0 >= 0 holds vacuously). Add require!(effective_pool_a > 0 && effective_pool_b > 0, AmmError::EmptyPoolReserve) before computing output, so solvency no longer depends on the deposit floor making a zero reserve unreachable. The Kani harness that characterizes the drain is kept as the justification for the guard. Both programs cargo-check cleanly. Update the crate READMEs and the root README to describe the findings as fixed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KaahCx3pNdwvM6EycqZBPa
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds Kani formal-verification proofs to every program under
finance/, in the spirit of aeyakovenko/percolator. Each program gets a standalonefinance/<program>/kani-proofs/crate that models its pure money-math and proves the invariants exhaustively over all inputs (within bounds), rather than sampling them with unit tests.40 proof harnesses across 7 programs, all verifying green. Two non-exploitable edge cases the proofs surfaced are fixed in the programs (not just documented) — see below.
knever decreasesΣ fills + remaining == incomingEach crate ships a
README.md(harness list, invariants, bounds, timings) and plaincargo testunit tests so the models are useful even without Kani installed.Program hardenings (the two findings, fixed)
1. escrow —
close_offer_accountlamport ordering (finance/escrow/native/program/src/utils.rs)The function zeroed the source account's lamports before the fallible
checked_addthat credits the destination, so an overflow returnedErrafter the source was already zeroed — transiently destroying lamports (safe on-chain only because the runtime reverts failed instructions). Fix: compute-then-commit — run thechecked_addfirst and mutate nothing until it succeeds. Lamport conservation now holds with equality on every path from the function's own logic;proof_close_offer_conserves_lamports_unconditionallyproves it with no precondition.2. token-swap (AMM) — zero-reserve drain (
finance/token-swap/anchor/programs/token-swap/src/instructions/swap_tokens.rs)When an input-side effective reserve is
0, the constant-product curve outputs the entire opposite reserve, and the end-of-swaprequire!(new_invariant >= invariant)guard doesn't catch it (pre-tradek = 0, so0 >= 0holds vacuously). Fix:require!(effective_pool_a > 0 && effective_pool_b > 0, AmmError::EmptyPoolReserve)before computingoutput, so solvency no longer depends on the deposit floor making a zero reserve unreachable. (Reaching that state was already prevented byMINIMUM_LIQUIDITY; this is defense-in-depth on a fund-draining path.)Both programs
cargo checkcleanly. No#[kani::should_panic]is used anywhere: a should-panic harness inverts the maintenance signal (fixing the code makes the test fail), so both findings are encoded as positive proofs of the now-stronger invariants.CI — runs weekly, not per push/PR
The new
.github/workflows/kani.ymlruns the fullcargo kaniverification across all 7 finance crates on a weekly schedule (Mondays 06:00 UTC) plus manualworkflow_dispatch. The workflow header documents why: most proofs verify nonlinear 128-bit arithmetic (constant-product curves,mul_divwith a symbolic divisor, integer sqrt, pari-mutuel payouts), which is the worst case for a bit-precise model checker — individual harnesses take tens of seconds and a full crate runs for minutes, far too slow to gate every push. A fastcargo testjob still runs on every push/PR to catch model regressions early.Developer experience
A
SessionStarthook (.claude/hooks/session-start.sh) auto-installs the Kani toolchain in Claude Code on the web sessions (idempotent, remote-only), socargo kaniworks without a manual install step.Notes for reviewers
require!) is defense-in-depth on an edge that's likely already unreachable — happy to drop just that one line if you'd prefer to keep the AMM example minimal.🤖 Generated with Claude Code
Generated by Claude Code