AI writes your code.
Our tools prove that code is correct.
Midspiral is building the correctness layer for AI-generated software. Open-source tools that mathematically guarantee your code does what it says.
Humans define what should be built.
AI handles implementation.
Machines guarantee correctness.
Open-source tools for provable correctness.
An npm package that adds mathematical verification to AI coding sessions. Your AI agent writes both the code and its proof. An external verifier checks the proof automatically. What can't be proven doesn't compile.
Annotate ordinary TypeScript with //@ specification comments — preconditions, postconditions, invariants. LemmaScript compiles them into Lean 4 or Dafny. Works on greenfield and existing codebases.
The shared verification engine behind Midspiral's tools. Manages proof orchestration, daemon lifecycle, and the bridge between AI agents and external verifiers.
Coming soon
A proof guarantees the code is correct — but does it guarantee what you actually meant? claimcheck translates proofs back to plain English and compares them against your original requirements. Narrows the gap between "verified" and "intended."
The methodology underneath. Verified state kernels for web applications — undo/redo, multi-user collaboration, reconciliation — proven correct and compiled to JavaScript. The foundation lemmafit is built on.
Dafny-to-TypeScript API compiler. Takes verified Dafny modules and compiles them into callable TypeScript APIs — Init(), Dispatch(), Present() — so your frontend can use proven logic directly.
Principles across everything we build.
The human states intent. The machine proves it.
You describe what should be true. The tools generate code and a mathematical proof that it holds — for all possible inputs, not just the ones you tested.
External verification, not self-grading.
The AI proposes. A separate, deterministic process checks. No model grades its own work. The verifier is outside the loop, and it doesn't negotiate.
Complexity stays under the hood.
Our tools use formal methods internally, but you don't need to be a formal methods expert. You write requirements in plain language. The proof machinery is invisible.
Open source, built in public.
Every tool is open source. Every insight is published. We document what we learn as we learn it — the wins, the failures, and the open questions.
We build in public.
LemmaScript: A Verification Toolchain for TypeScript via Dafny
LemmaScript compiles TypeScript to Dafny (or Lean) for verification, keeping the executable pipeline unchanged while adding a complementary path that certifies correctness.
Formally Verified AI-Generated Code is Already Here
Formally verified AI-generated code isn't a distant, future bet — it's already possible. We're just refining now.
Introducing lemmafit: A Verifier in the AI Loop
lemmafit is an open-source npm package that adds formal verification to AI coding workflows. Install it, prompt Claude Code, and get mathematically proven logic compiled to TypeScript.
Follow the build.
We send occasional updates when we discover or ship something worth sharing.
Thanks for subscribing!