A recap of our LemmaScript workshop at Antithesis HQ in San Francisco. Now that AI has solved for speed, volume, and the expertise gap, correctness is the next frontier — and the room was ready for it.
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 isn't a distant, future bet — it's already possible. We're just refining now.
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.
A verified proof guarantees the code is correct, but does it guarantee what you actually meant to guarantee? claimcheck uses round-trip informalization to narrow the gap between formal proof and original intent.
Formal verification catches completeness bugs that property-based testing struggles to reach.
Pushing formal verification into collaborative state — concurrent users, stale views, conflicts, and integration with Supabase
A React developer builds a real app using formal verification. This is a chronological build log: the spec design, the integration hell, and what it subjectively felt like.
Verified kernels, written in Dafny and compiled to JavaScript, for correct-by-construction state in interactive web applications
How AI approaches code architecture and how immutable constraints will transform AI programming.