Skills
.Work. You
Rest

leanstral

Community

Lean 4 formal verification for Solana programs

Software Engineering#formal verification#rust#lean#proof#solana
Authorabishekk92
Version1.0.0
Installs0

System Documentation

What problem does it solve?

Verifying the correctness of Solana smart contracts is complex and time‑consuming, requiring deep expertise in both blockchain logic and formal methods.

Core Features & Use Cases

  • Automated SPEC.md generation from existing IDLs or source code.
  • Lean 4 model and proof construction for access control, state machines, CPI correctness, and arithmetic safety.
  • Iterative compilation with lake build, allowing Claude to refine proofs until they succeed.
  • Hard sub‑goal solving via the Mistral Leanstral model, filling sorry markers automatically.
  • Use case: A developer can run the skill to produce machine‑checked proofs that their escrow program cannot be exploited.

Quick Start

Ask Claude to formally verify my Solana program using the leanstral skill.

Dependency Matrix

Required Modules

None required

Components

Standard package

💻 Claude Code Installation

Recommended: Let Claude install automatically. Simply copy and paste the text below to Claude Code.

Please help me install this Skill:
Name: leanstral
Download link: https://github.com/abishekk92/leanstral-solana-skill/archive/main.zip#leanstral

Please download this .zip file, extract it, and install it in the .claude/skills/ directory.
View Source Repository

Agent Skills Search Helper

Install a tiny helper to your Agent, search and equip skill from 471,000+ vetted skills library on demand.