Show HN: LemmaScript, a verification toolchain for TypeScript via Dafny

Category: devtools

Tags: formal-verification, typescript, proof-assistant, static-analysis, dafny

Score: 7.0/10 (Innovation: 8, Technical: 8, Documentation: 7, Utility: 5)

LemmaScript is a verification toolchain that allows writing TypeScript with specification annotations, then generates verifiable code in Dafny or Lean 4. It's interesting because it brings formal verification to mainstream TypeScript development, enabling mathematical proofs of correctness for real-world applications like web apps, security middleware, and algorithms.

Target audience: backend devs, security engineers, library authors

Repository: https://github.com/midspiral/LemmaScript · TypeScript · MIT · 15 stars

View on Hacker News