We present the motivation, design, implementation and application of LemmaScript, a verification toolchain for TypeScript. LemmaScript adds verified contracts to TypeScript, and those contracts are checked in parallel to the execution path by translation to Dafny or Lean (via Velvet) and relying on LLM-based agents to complete the proofs on the verification-aware target. We recorded 26 case studies in LemmaScript, both greenfield and brownfield. We find that LemmaScript offer a spectrum of ways of AI-assisted verified programming, from leaving the verified contracts to the agent to desinging specifications in natural language upfront.