Formal verification for AI-generated code. Automatically extracts correctness properties from pure functions, translates them into Lean 4 theorems, and machine-checks them with Mathlib — so you get mathematical proof, not just tests, for the logic your AI coding agent produces. Works with any LLM — Claude, GPT-4, Gemini, Llama, Mistral, or any OpenAI-compatible endpoint.