Skip to main content
New Shallow embedding: why LemmaScript translates TypeScript straight into Dafny →
the correctness layer for ai-generated software

More confidence, less review

Ship harder, faster, cheaper with a verifier in the loop

Give your agents the tooling they need to write correct, performant, and well-structured code with fewer iterations.

Learn more →
REVIEW LOAD VS. CONFIDENCE BEFORE WITH A VERIFIER IN THE LOOP HUMAN REVIEW confidence WEEKS →
SPEC + IMPLEMENTATION AUDIT TEST DEPLOY RUNTIME OVER TIME /lemmascript /claimcheck /crosscheck CI /guard /seal skills — guiding the agent throughout

“I am super happy with LemmaScript. We ship tons of code in Hiya, and have LemmaScript make us feel comfortable with doing so.
I can't ship code without LemmaScript from now on.”

Steve Nguyen

Out of the lab,
into your stack.

  • SMT solvers decision procedures
  • Autoformalization English → logic
  • Program verification code meets spec
  • Model checking every reachable state
  • Symbolic execution all paths at once
  • Refinement types types that carry facts
  • Browser
  • Node
  • GitHub Actions
  • Deno
  • Agent harnesses
  • Bun
  • Workers
  • npm
  • Electron
  • React
  • Containers
  • etc

Want it in your stack? Tell us about your use case →

Open-source tools

Each covers a stage of the pipeline — use one, or run the whole chain.

  • /LemmaScript v0.6.5 Contracts in your TypeScript, checked by an external prover. GitHubnpmDocs
  • /claimcheck v0.2.1 Checks the plain-English intent against the formal spec. GitHubnpm
  • /crosscheck v0.1.0 Fuzzes the running JavaScript against the verified model. GitHubnpm
  • /guard v0.1.0 Compiles verified preconditions into runtime boundaries. GitHubnpm
  • /seal v0.1.0 Append-only guarantee ledger: contracts can be added to, never weakened. GitHub
  • CI Reusable GitHub Actions workflow: regenerate, verify, fail the build if stale. GitHub
  • skills Agent skills for the whole toolchain, in plain markdown. GitHub
  • /LemmaSwift coming soon Contracts and proof, brought to Swift.
Request a tool →

Field notes on verified software.

AUG 2026

Shallow embedding: why LemmaScript translates TypeScript straight into Dafny

Most 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.

read →
JUN 2026

Talking Software Correctness at Antithesis SF

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.

read →
APR 2026

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.

read →
See all posts →

Explore verification