7 packages
claimcheck
Does a Dafny lemma actually mean what a natural language requirement says? Dafny can verify proofs, but it can't verify meaning. Claimcheck fills that gap.
emira
Emira — coming soon from Midspiral
eslint-plugin-with-lemmascript
Formally-verified ESLint rules, proved with LemmaScript. no-forbidden-reach enforces architecture boundaries through any import chain — not just direct imports.
hono-rate-limiter-with-lemmascript
Formally-verified sliding-window rate limiter for Hono, proved with LemmaScript. Never more than `limit` admissions in any window of length W — the cross-boundary 2× burst a fixed-window counter allows is provably impossible.
lemmafit
Make agents prove that their code is correct.
lemmascript
A verification toolchain for TypeScript — generates Lean 4 or Dafny from annotated TS
lemmascript-claimcheck
claimcheck for LemmaScript: vet that a function's informal //@ contract faithfully describes its verified //@ requires/ensures, and emit a guarantees report.