invariant-gen: Automatically Generate Security Invariants for Solana Smart Contracts Using Large Language Models

invariant-gen is a tool that combines Retrieval-Augmented Generation (RAG) and local Large Language Model (LLM) inference, designed to automatically generate formal security invariants for Solana Anchor smart contracts. It supports multi-format outputs including QEDSpec, Kani, and JSON, and enables fully localized contract security audits, helping to lower the technical barrier of formal verification so that ordinary developers can also access expert-level security audit capabilities.

Blockchain smart contracts are hard to modify after deployment, so security is crucial. The Solana ecosystem uses the Anchor framework to simplify development, but complex contract logic still makes vulnerabilities easy to occur. Traditional manual audits are costly and time-consuming; while formal verification is effective, writing security invariants requires deep professional knowledge and a lot of manual work, which becomes a barrier to its popularization.

invariant-gen uses RAG technology to encode professional audit knowledge into a retrievable knowledge base, and combines LLMs to generate targeted invariants. Its workflow includes: 1. Knowledge base construction (extract audit reports into structured JSON, generate embedding vectors for storage); 2. Contract analysis (convert Anchor source code to llms.txt, parse instruction processors to generate embeddings); 3. Semantic retrieval (match the most relevant audit cases using cosine similarity); 4. Invariant generation (generate multi-format outputs by combining context and source code). The tool supports fully localized operation (QVAC framework: GTE-Large requires 700MB memory, Qwen3-0.6B requires 400MB) and can also be combined with cloud services.

invariant-gen supports three output formats: QEDSpec specification files (including clauses like guard and requires), Rust test code for the Kani verification framework (directly usable for formal verification), and structured JSON (including metadata, confidence, etc.). The tool provides verification commands—for example, invariant-gen validate can compile and check the syntax of Kani assertions to ensure the generated code is usable.

The innovations of invariant-gen include: 1. Combining RAG with formal verification to guide generation using historical audit cases; 2. Semantic similarity matching (embedding vectors) to detect logically similar vulnerabilities; 3. Flexible deployment (pure local/cloud/hybrid); 4. Progressive workflow (dry-run preview, single instruction generation, etc.).

invariant-gen is suitable for: 1. Early problem detection during contract development; 2. Self-checking and fixing obvious vulnerabilities before audits; 3. Accelerating candidate invariant generation in security research; 4. Assisting in understanding formal invariant writing in education and training.

Current limitations: Generation quality depends on the relevance of audit cases, insufficient coverage of novel vulnerabilities; limited inference capabilities of local models; only supports Solana Anchor. Future directions: Expand the knowledge base; integrate verification feedback loops; support more formats and chains; develop IDE plugins.

invariant-gen applies LLM and RAG technologies to smart contract security, lowering the barrier to formal verification and benefiting more developers. It not only improves the security of individual contracts but also helps systematically enhance the security level of the entire ecosystem.