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.

Currently optimized for Claude Code with React + TypeScript projects. The AI doesn't always get proofs right on the first try, but the verification loop catches mistakes automatically. Works with both new projects (lemmafit init) and existing codebases (lemmafit add).

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

Yes. lemmafit add adds verification to an existing project — it models your code, writes Dafny proofs for your core logic, and compiles them back to TypeScript. The add functionality is still in preview mode so you may run into unexpected snags.

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.