lean-agentic

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!

• ✅ 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

🎯 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!