Set Up Local Agents for Formal Verification in Lean

Apr 23, 2025

Building formal verification tools requires powerful language models that can assist with complex reasoning tasks. This post will guide you through setting up a minimal local agent that can be used for formal verification of smart contracts or mathematical proofs.

Prerequisites

Before getting started, you'll need to:

Download and install Ollama - a tool for running language models locally
Install uv - a fast Python package manager

Step 1: Download a Model

Ollama lets you run various language models locally. For formal verification work, consider one of these options:

# LLMLean finetuned model (8.5 GB) - specialized for theorem proving
ollama pull wellecks/ntpctx-llama3-8b

# Qwen model (4.4 GB) - good general reasoning capabilities 
ollama pull qwen2:7b

# Lightweight Llama model (2.0 GB)

Start the Ollama server:

Step 2: Set Up the Environment

Clone the repository and set up a virtual environment:

# Clone the repository
git clone https://github.com/formalmind/formal-agent.git

# Navigate to the project directory
cd agents

# Create a virtual environment
uv venv

# Activate the environment
source

Step 3: Initialize Your Model

You can now use the formal verification agent in your projects. The sample code below demonstrates how to use different models to solve a simple theorem about coprime numbers:

from agents.llmlean import LLMLean
from agents.qwen7b import Qwen7b
from agents.llama3 import Llama3
from agents.prompt import make_lean_tac_prompt

# Define a theorem and context
ctx = """import Mathlib.Data.Nat.Prime

theorem test_thm (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 := by
"""
state = """m n : ℕ
h : Nat.Coprime m n
⊢ Nat.gcd m n = 1
"""
# Create a prompt for the model
prompt = make_lean_tac_prompt(ctx, state)

# Initialize the models
agent = LLMLean()  # Specialized for theorem proving
agent2 = Qwen7b()  # Alternative model
agent3 = Llama3()  # Lightweight model

# Get responses from each model
print(agent.get_messages(prompt))

Step 4: Run Your Agent

Execute your agent with:

The output will show you the tactics suggested by the model to prove the theorem:

rw [gcd_eq_one_iff_coprime h, ← one_mul (gcd _ _), Nat.mul_comm n, gcd_comm]

The Cost-Effective Approach to Formal Verification

Building secure software has become increasingly accessible, and there's no longer any excuse for failing to identify critical bugs. As I shared in a recent LinkedIn post, we're reaching a stage where you can simply instruct an AI agent to "Please ensure my software/service is secure" and get meaningful results.

These agents can:

Start logical processes and provide proofs with specific guarantees
Analyze application logic within its context
Construct formal proofs by examining the context and reviewing all functions in your code
Transform informal specifications into formal proofs

However, cloud-based AI infrastructure remains expensive. Using services like Claude API can cost significant amounts - I spent $1.39 in just 25 minutes for a handful of inferences in Lean! Commercial deployment options often start at around $0.70 per hour, which translates to approximately $500 per month - a steep investment for early-stage startups.

The solution: stick to local setups. Even modest hardware like a 16GB Intel MacBook can run inference effectively. The setup described in this post costs $0 to operate (apart from your electricity bill), making formal verification accessible to everyone.

Next Steps

With this local setup, you can now start building more sophisticated formal verification tools. You could:

Create specialized prompts for software verification
Develop agents that can translate your code e.g Solidity to Lean theorems
Build interactive proof assistants that guide users through the verification process

Local agents provide privacy, lower latency, customization options, and most importantly, a cost-effective approach to formal verification that makes building secure software the standard, not the exception.