FAQ

An open-source tool that lets AI agents write formally verified logic for your apps. You describe what you want in plain English, and the AI writes both the code and a mathematical proof that it's correct. The verified logic compiles to TypeScript for use in your React app.

Tests check specific inputs you think of. Formal verification proves properties hold for all possible inputs. They're complementary — lemmafit handles your core logic (state machines, business rules, data integrity), and you still write tests for integration, UI, and everything else.

No. The AI writes the Dafny code and proofs. You describe what you want in natural language. The verification daemon runs automatically in the background — you don't interact with Dafny directly.

Any app where core logic correctness matters — task managers, workflow engines, billing systems, anything with state machines or business rules. lemmafit verifies the logic; your AI wires it into a React UI.

This is a working proof of concept, not a finished product. Currently: greenfield projects only (React + TypeScript), optimized for Claude Code, and the AI doesn't always get proofs right on the first try (the verification loop helps). Existing codebase support and other AI tools are on the roadmap.

Currently Claude Code only. The hook system, skills, and instructions are Claude Code-specific. Support for other AI coding tools (Cursor, Windsurf, etc.) is planned.

Not yet. Right now you need to start with lemmafit init. Support for retrofitting verification onto existing codebases is in progress.

Yes. Open source, MIT licensed. You'll need a Claude Code subscription to use the AI agent.

A human-readable breakdown of your app's properties: which are mathematically proven, which rely on assumptions, and which aren't covered by verification (like UI behavior). It makes the boundary between verified and unverified logic explicit.