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.
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. Catches 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.
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.
Introducing lemmafit: A Verifier in the AI Loop
An npm package that forces AI to prove its code is correct before it compiles. Works with Claude Code today.
claimcheck: Narrowing the Gap between Proof and Intent
Proofs verify code, but do they verify what you meant? Round-trip informalization catches the gap.
The Intent Envelope: Proofs for Completeness
Formal verification catches completeness bugs that property-based testing can't reach.
Follow the build.
We send occasional updates when we discover or ship something worth sharing.
Thanks for subscribing!