Lean-Agentic: Formally Verified Agentic Programming Language

A hybrid programming language combining Lean4's formal verification with blazing-fast compilation, Ed25519 cryptographic proof signatures, actor-based agent orchestration, AI-driven optimization, and vector-backed agent memory.

Developed by: ruv.io | github.com/ruvnet

---

🚀 NPM Package Available!

lean-agentic is now available as an npm package with full CLI and MCP support!

# Install globally
npm install -g lean-agentic

# Or use with npx
npx lean-agentic --help

Features: - ✅ CLI Tools: Interactive REPL, benchmarks, theorem proving - ✅ MCP Integration: 10 tools for Claude Code (5 core + 5 AgentDB) - ✅ AgentDB Integration: Vector search, pattern learning, self-learning theorems - ✅ WASM Powered: Works in Node.js and browsers - ✅ File Persistence: Store and learn from theorems

NPM: https://npmjs.com/package/lean-agentic

---

🎯 Vision

Build trustworthy autonomous agents at scale by combining four critical properties rarely seen together:

• ⚡ Speed: Sub-100ms compilation, nanosecond-scale message passing, 150x faster equality checks
• 🛡️ Safety: Formally verified kernels with zero runtime overhead, minimal trusted computing base
• 🔐 Trust: Ed25519 cryptographic proof signatures, multi-agent consensus, tamper detection, non-repudiation
• 🧠 Intelligence: AI-driven optimization, cost-aware routing (40%+ savings), pattern learning, self-learning from proofs

✨ Key Features

🔐 NEW: Ed25519 Proof Attestation (v0.3.0)

Cryptographic signatures for formal proofs - Add trust, authenticity, and non-repudiation to your theorems!

// Sign a proof with your identity
let agent = AgentIdentity::new("researcher-001");
let signed_proof = agent.sign_proof(proof_term, "Identity function", "direct");

// Verify: Mathematical + Cryptographic
let result = signed_proof.verify_full(&trusted_agents);
assert!(result.mathematically_valid && result.cryptographically_valid);

// Multi-agent consensus (Byzantine fault tolerance)
let consensus = ProofConsensus::create(signed_proof, validators, threshold)?;
assert!(consensus.verify());

Features: - 🔑 Agent Identity - Ed25519 keypairs for proof signing - ✅ Dual Verification - Mathematical (type checking) + Cryptographic (Ed25519) - 🤝 Multi-Agent Consensus - Byzantine fault tolerant proof validation - 🛡️ Tamper Detection - Automatic cryptographic integrity verification - ⚡ Fast - 152μs keygen, 202μs sign, 529μs verify - 📊 Chain of Custody - Track proof provenance with signatures - 🔍 Non-Repudiation - Agents can't deny proofs they signed

Example: cargo run --example ed25519_proof_signing

📦 NPM Package & CLI

Version: 0.3.0 | Size: 88.6 KB | Status: Published

Quick Start

# Interactive demo
npx lean-agentic demo

# REPL
npx lean-agentic repl

# Performance benchmarks
npx lean-agentic bench

# MCP server for Claude Code
npx lean-agentic mcp start

AgentDB Integration (NEW!)

# Initialize self-learning database
npx lean-agentic agentdb init

# Store theorems with vector embeddings
npx lean-agentic agentdb store

# Search using semantic similarity
npx lean-agentic agentdb search "identity function"

# Learn patterns from successful proofs
npx lean-agentic agentdb learn

# View statistics
npx lean-agentic agentdb stats

Features: - 🧠 Self-Learning: Learns from every proof stored - 🔍 Vector Search: 90% semantic similarity accuracy - 📊 Pattern Recognition: Identifies successful strategies - 💾 Persistence: JSON database with auto-save - 📈 Analytics: Success rates, confidence scores, statistics

📋 Complete NPX Commands Reference

Core Commands:

npx lean-agentic demo           # Interactive demonstration
npx lean-agentic repl           # Interactive REPL for theorem proving
npx lean-agentic bench          # Performance benchmarks
npx lean-agentic --help         # Show all available commands
npx lean-agentic --version      # Display version information

AgentDB Commands:

npx lean-agentic agentdb init                    # Initialize database
npx lean-agentic agentdb store                   # Store theorem (default: identity)
npx lean-agentic agentdb store --type <type>     # Store with specific type
npx lean-agentic agentdb search "<query>"        # Semantic search
npx lean-agentic agentdb search "<query>" -l 10  # Search with custom limit
npx lean-agentic agentdb learn                   # Analyze patterns
npx lean-agentic agentdb stats                   # View statistics

MCP Server:

npx lean-agentic mcp start      # Start MCP server for Claude Code

🔌 MCP Tools Reference (10 Total)

Core Theorem Proving Tools (5):

1. create_identity - Create identity function (λx:Type. x)
2. Returns: Term representation with TermId

3. Use: Basic theorem construction

4. create_variable - Create De Bruijn indexed variables

5. Input: Variable index (number)

6. Returns: Variable term with TermId

7. demonstrate_hash_consing - Show hash-consing performance

8. Returns: Performance comparison (150x faster equality)

9. Use: Verify optimization is working

10. benchmark_equality - Run equality check benchmarks

11. Returns: Timing data for term comparisons

12. Use: Performance validation

13. get_arena_stats - Get arena allocation statistics

14. Returns: Memory usage, allocation count, deduplication ratio
15. Use: Memory optimization analysis

AgentDB Integration Tools (5):

1. agentdb_init - Initialize AgentDB database
2. Input: Optional database path
3. Returns: Initialization status

4. Use: Setup before storing theorems

5. agentdb_store_theorem - Store theorem with vector embeddings

6. Input: Theorem object (type, statement, proof, strategy)
7. Returns: Stored theorem with ID and embeddings

8. Use: Persist theorems for learning

9. agentdb_search_theorems - Semantic similarity search

10. Input: Query string, limit (optional)
11. Returns: Similar theorems with similarity scores

12. Use: Find related theorems (90% accuracy)

13. agentdb_learn_patterns - Analyze patterns with ReasoningBank

14. Returns: Learned patterns, confidence scores, success rates

15. Use: Identify successful proof strategies

16. agentdb_get_stats - Get database statistics

    • Returns: Total theorems, success rate, storage size, types
    • Use: Monitor database health and growth

MCP Resources (3): - arena://stats - Arena memory statistics - system://info - System information - agentdb://status - AgentDB connection status

MCP Prompts (2): - theorem_proving - AI-optimized theorem proving guidance - pattern_learning - ReasoningBank learning strategies

Using MCP Tools in Claude Code:

# Add MCP server to Claude Code
claude mcp add lean-agentic npx lean-agentic mcp start

# Tools become available automatically in Claude Code
# Use natural language to invoke tools:
# "Create an identity function using lean-agentic"
# "Store this theorem in AgentDB"
# "Search for similar theorems about identity"
# "Show me arena statistics"

🏗️ Core Language Features

Lean4-Style Dependent Type Theory

• Full dependent types with universe polymorphism
• Bidirectional type checking (synthesis + checking modes)
• Implicit argument resolution
• Pattern matching with exhaustiveness checking
• Inductive types with recursors
• Proof-carrying code

Hash-Consed Term Representation (150x Speedup)

// All occurrences of identical terms share ONE allocation
let x1 = arena.mk_var(0);  // Allocates new term
let x2 = arena.mk_var(0);  // Reuses existing term
assert_eq!(x1, x2);        // Same TermId, 0.3ns equality check vs 45ns structural

Performance: - 0.3ns term equality (hash comparison) - 85% memory reduction via deduplication - 95%+ cache hit rate in practice - 6.9:1 deduplication ratio on real code

Minimal Trusted Kernel (<1,200 lines)

Only the type checker and conversion checker are trusted. Everything else can have bugs without compromising soundness: - typechecker.rs - 260 lines - conversion.rs - 432 lines - term.rs + level.rs - 508 lines - Total: ~1,200 lines of safety-critical code

⚡ Compilation System

Sub-100ms Incremental Builds

• Salsa-based query system with red-green dependency tracking
• Function-level granularity for surgical recompilation
• LRU + disk caching (80%+ hit rate on typical workflows)
• Streaming compilation processes functions as parsed

Cache Performance: - Memory cache: 200MB, 0.1-1ms latency - Disk cache: 2GB, 2-5ms latency - Cache miss: 5-20ms per function

Dual-Path Backend

• Cranelift for debug builds: 60-180ms, fast iteration
• LLVM for production: 1-5s, maximum optimization
• Position-independent code enables in-place binary patching
• WASM-first design with native as optimization target

🤖 Agent Runtime

Nanosecond-Scale Message Passing

// Zero-copy message sending with compile-time safety
let msg = Message::<Request, Iso>::new(request);  // Isolated capability
agent.send(msg).await?;  // <200ns send latency

Performance Targets: - <500ns agent spawn (local) - <200ns message send latency - 100K+ msg/s throughput per core - <10ms P99 end-to-end latency

Reference Capabilities (Pony-Inspired)

Type-level enforcement of data race freedom: - iso (Isolated): Unique read/write, sendable across threads - val (Value): Immutable, freely shareable and sendable - ref (Reference): Local read/write, NOT sendable - tag (Tag): Identity only, for actor references

Zero runtime overhead - all capability checking at compile time.

Work-Stealing Scheduler

• Per-core local queues (256 tasks) with LIFO slot optimization
• Global MPMC queue for overflow and stealing
• Randomized victim selection with throttled stealing
• Predictive scheduling with agent execution profiles
• Go-style G-M-P model with Tokio integration

8 Orchestration Primitives

// Spawn agents
let agent = spawn(TradingAgent::new(), 1000).await?;

// Send messages
signal(agent, PriceUpdate { symbol, price }).await?;

// Async coordination
let result = await(future).await?;

// Channels
let (tx, rx) = channel::<Quote>(1000);

// Quorum consensus
let votes = quorum(agents, threshold, request, timeout).await?;

// Consistent sharding
let target = shard(key, agents);

// Distributed leases
with_lease(resource, ttl, || trade.execute()).await?;

// Mesh broadcasting
broadcast(agents, alert, fanout).await?;

🧠 AI-Driven Optimization

LLM Compiler Integration (Meta 13B)

• XLA AOT compilation (no runtime dependencies)
• ML-guided auto-vectorization with GNN + DRL
• Mutation-guided test synthesis (93%+ mutation score)
• SMT-based validation with Z3 solver
• <100ms inference in batch mode

4-Tier JIT Compilation

Adaptive optimization based on runtime profiling:

Tier	Compile Time	Speedup	When to Use
Tier 0 (Interpreter)	0ms	1x	Cold code, immediate execution
Tier 1 (Baseline JIT)	1-5ms	5-15x	Warm code (10+ invocations)
Tier 2 (Optimizing JIT)	10-50ms	20-50x	Hot code (100+ invocations)
Tier 3 (Max-Opt JIT)	100-500ms	50-200x	Very hot code (1000+ invocations)

Features: - Profile-guided optimization with type feedback - On-stack replacement (OSR) for hot loops - Speculative optimization with deoptimization - Inline caching for dynamic dispatch

Multi-Lane Cost Routing (40%+ Savings)

Dynamic provider selection for AI inference:

Lane	Cost per 1K tokens	Latency P50	Use Case
onnx_local	$0.00	15-30ms	Privacy, offline, cost-sensitive
anthropic	$0.10	200-500ms	Quality, complex reasoning
openrouter	$0.05	100-300ms	Balance cost/quality

Features: - Real-time cost tracking with quota enforcement - Adaptive routing with reinforcement learning - <5% cost variance from predictions - Automatic fallback on provider failures

Demonstrated Savings:

// Example: 10K inference requests
// All anthropic: $1.00
// Multi-lane optimized: $0.58 (42% savings)
// With <5% variance from prediction

💾 AgentDB Vector Memory

Sub-Millisecond Retrieval

• Qdrant/HNSW integration with M=16, ef=64
• <10ms P99 latency for 1M vectors
• 1536-dimensional embeddings (OpenAI ada-002)
• Cosine similarity with exact + approximate search

Episodic Memory with Causal Graphs

// Store episode with causal tracking
store_episode(Episode {
    context: "User asked about trading strategy",
    action: "Analyzed market data and recommended approach",
    outcome: "Successful trade with 3% profit",
    causal_links: [prev_episode_1, prev_episode_2],
    entities: [entity_market, entity_user],
}).await?;

// Retrieve with explainable recall
let result = retrieve_episodes("trading strategy", 10).await?;
// Returns: memories + similarity scores + causal chains + reasoning

Memory Types: - **Epis