LemmaScript contracts by example
Nov 07, 2026Examples of LemmaScript contracts for TypeScript: conservation, rounding, state invariants, order independence, decision procedures, and agent safety.
Field notes on verified software.
-
-
Shallow embedding: why LemmaScript translates TypeScript straight into Dafny
Aug 12, 2026Most verification tools lower your program into logic formulas for a solver. LemmaScript turns it into readable, high-level Dafny instead. It's an unconventional trade made on purpose, because the proofs are written by LLMs.
-
Talking Software Correctness at Antithesis SF
Jun 09, 2026A 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: A Verification Toolchain for TypeScript via Dafny
Apr 22, 2026LemmaScript 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
Apr 21, 2026Formally 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
Mar 07, 2026lemmafit 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.
-
claimcheck: Narrowing the Gap between Proof and Intent
Feb 17, 2026A 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.
-
The Intent Envelope: Proofs for Completeness, Not Just Soundness
Jan 26, 2026Formal verification catches completeness bugs that property-based testing struggles to reach.
-
Verifying State & Reconciliation in Collaborative Web Apps
Jan 13, 2026Pushing formal verification into collaborative state — concurrent users, stale views, conflicts, and integration with Supabase
-
Building a React App with Formally Verified State
Dec 30, 2025A 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.
-
From Intent to Proof: Dafny Verification for Web Apps
Dec 26, 2025Verified kernels, written in Dafny and compiled to JavaScript, for correct-by-construction state in interactive web applications