1. Look for .claude/svk-meta.json in the current project. If it doesn't exist, skip this check entirely.
2. Read the svk_repo path and installed_version from the metadata file.
3. Run: git -C <svk_repo> fetch --tags --quiet 2>/dev/null
4. Run: git -C <svk_repo> tag --sort=-v:refname | head -1 to get the latest tag.
5. Compare the installed version against the latest tag (strip the leading v).
6. If they match, skip — the user is up to date.
7. If the latest tag is newer, show this message ONCE (never repeat in this session):

SVK Update Available: v{latest} is available (you're on v{installed}).

• Update now: I can pull and reinstall the changed skills in this session
• Update later: Start a new chat and run /SVK:update

8. If the git commands fail (offline, repo moved, etc.), skip silently. Never show errors from version checking.

Important: Do NOT block or delay the user's actual command. Perform this check, show the notification if needed, then proceed with the command they invoked. </svk-version-check>

Book of Knowledge

Math verification and economic invariant proving for Solana/Anchor programs.

"Knowledge is the greatest weapon."

Artifact Convention

All BOK artifacts are stored in .bok/ at the project root — the same directory that contains Cargo.toml or Anchor.toml. This is NOT under .claude/.

<project-root>/
├── .bok/                  ← BOK artifacts go here
│   ├── STATE.json
│   ├── INDEX.md
│   ├── invariants/
│   ├── confirmed-invariants/
│   ├── worktree/
│   ├── results/
│   └── reports/
├── .claude/               ← Skill code lives here (NOT for artifacts)
├── Cargo.toml
└── programs/

IMPORTANT: Never create BOK artifacts under .claude/. The .claude/ directory contains skill definitions and commands — it is not an artifact output location.

What BOK Does

BOK systematically verifies that your program's arithmetic is correct and economic properties hold. It uses three verification tools in layers: Kani for formal proofs (checks ALL possible inputs), LiteSVM for runtime tests against the actual SVM, and Proptest for rapid property-based stress testing with thousands of random inputs. Every invariant comes with a plain-English explanation and concrete exploit scenario so you learn something from every run.

When to Use

• Pre-deployment math review — Verify arithmetic before shipping
• After SOS flags arithmetic issues — BOK can formally prove or refute SOS findings
• New DeFi math — Swaps, fees, staking, LP, oracles, liquidations, bonding curves
• Token economics verification — Prove conservation of value, share fairness, rate consistency

Pipeline Overview

Verification Tools

Graceful Degradation

If Kani is not installed and the user declines installation, BOK runs with LiteSVM + Proptest only. The report clearly flags that results are probabilistic (stress-tested), not formally proven, and recommends Kani for full assurance.

Worktree Workflow

All generated verification code lives in an isolated git worktree — your working tree is never touched. After execution, you choose: merge all tests, cherry-pick specific ones, or discard everything and keep only the report.

Cross-Skill Integration

• Reads GL docs — Uses specs to understand intended behavior, making invariant proposals more accurate
• Reads SOS findings — Prioritizes verification around areas SOS flagged as risky
• SOS reads BOK reports — Skips re-analyzing formally verified math, focuses on non-math attack vectors

Getting Started

/BOK:scan       — Start here. Indexes your code and checks prerequisites.
/BOK:analyze    — Proposes invariants with explanations.
/BOK:confirm    — You review and approve before any code is generated.
/BOK:generate   — Creates verification code in an isolated worktree.
/BOK:execute    — Runs Kani, LiteSVM, and Proptest.
/BOK:report     — Compiles results, suggests fixes, offers test merge.