Solanalib

A Lean 4 library of formal models and verified theorems for Solana programs. Source on GitHub.

Start at the library overview, or jump straight to a layer:

• Primitives — atomic on-chain types (Pubkey, Lamports, Timestamp)
• Numeric — Q68.60 fixed-point arithmetic
• Account — the five-field on-chain account model
• Instruction — instruction + AccountMeta
• Finance — decay, growth, compounding, withdrawal caps
• SBPF — the sBPF ISA semantics

Generated with doc-gen4.