LemmaScript: A Verification Toolchain for TypeScript via Dafny
Summary
The article introduces LemmaScript, a verification toolchain that derives a verification model from TypeScript code by compiling to Dafny/Lean, enabling in-place property verification while preserving the original executable pipeline. It covers greenfield and brownfield verification examples (trimCookieWhitespace in Hono and a game decision procedure) and discusses practical caveats and future directions for applying verification in web applications.