Skip to main content
// blog

Dev notes

Notes from the team building LemmaScript: how contracts hold up in real TypeScript codebases, what agents do with them, and what we learn from shipping.

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

    // internals// design

RSS feed