---
title: "LemmaScript Changelog"
description: "Dated changes across the LemmaScript toolchain and ecosystem, generated from public repos."
last_updated: 2026-07-20
---

# LemmaScript Changelog

The 60 most recent entries across the LemmaScript toolchain and its ecosystem (of 232 total — see [the full changelog](https://lemmascript.org/changelog) for everything).

- **2026-07-13** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed how array `slice()` with negative indices is modeled: JavaScript counts negative slice indices from the end of the array, but the formal model clamped them to zero, so proofs about expressions like `arr.slice(-1)` could diverge from what the code actually does at runtime. The model now normalizes negative indices exactly the way JavaScript does, guarded by a new example covering negative start, end, and both-negative bounds. ([details](https://github.com/midspiral/LemmaScript/pull/171))
- **2026-07-13** · [lemmascript-skills](https://github.com/midspiral/lemmascript-skills) · Documentation: Edited the main lemmascript agent skill for completeness and removed redundant guidance, so coding agents driving the verification toolchain get a tighter, more accurate playbook. ([details](https://github.com/midspiral/lemmascript-skills/commit/9f789fdb838fa45f4455adff8949fa91bca83c8b))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Optional-chain comparisons against a literal now narrow in expression position too: a ternary like `entry?.kind === 'msg' ? entry.text : fallback` is understood to imply the base object is present in the then-branch (a missing base can never equal a real literal), and lowers to a proper match on the optional. This is the expression sibling of the existing `if (x?.kind !== 'msg') return` statement rule, sharing one core, and mirrors a pattern found in the flue case study. ([details](https://github.com/midspiral/LemmaScript/commit/05bd36f5750c02997cadd3a093bd25e80e0435c9))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Generalized early-return narrowing through `||` conditions from all-null-checks to arbitrary disjunctive guards: patterns like `if (!x || x.kind !== 'k') continue` now narrow `x` to present across the rest of the loop body, keeping the value checks as a residual condition. This covers the pervasive loop-skip idiom in strict-index-checked TypeScript, and one rule now subsumes what were previously three special cases. ([details](https://github.com/midspiral/LemmaScript/pull/169))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Completed JavaScript truthiness modeling for objects: `!x` on a non-optional object, array, map, set, or tuple now correctly lowers to `false` (all objects are truthy in JS), and a bare object in condition position lowers to `true`. This closes a spec gap and means a defensive `if (!obj)` guard in shipped code verifies as provably dead rather than being rejected. ([details](https://github.com/midspiral/LemmaScript/pull/168))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: A batch of language-fragment additions surfaced by real-world case-study code: `Array.prototype.findLastIndex`, bare `.sort()` with no comparator (modeled as a permutation instead of producing broken output), numeric `||` defaulting (`a || b` on numbers), and semicolon-separated field lists in `//@ declare-type` annotations to match TypeScript object-type syntax. ([details](https://github.com/midspiral/LemmaScript/pull/167))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Narrowing now handles code written under TypeScript's `noUncheckedIndexedAccess` flag: an array-element binding that is optional only because of the flag is modeled as the bounds-guarded optional it really is, so an in-bounds proof makes the 'missing' branch dead and safely-indexed brownfield code verifies as if the element type were total. A companion rule narrows the common `if (e?.disc !== lit) continue` loop idiom across the rest of the loop body. ([details](https://github.com/midspiral/LemmaScript/pull/164))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Heterogeneous tuples like `[string, number]` now compile to native backend tuples (Dafny pairs / Lean products) instead of collapsing to a sequence of the first element's type, which silently dropped the other slots' types. Covers tuple annotations, literals with heterogeneity inference, literal-index element access, and destructuring — verified end-to-end on both backends. ([details](https://github.com/midspiral/LemmaScript/pull/160))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed the Dafny backend rejecting `continue` statements it couldn't restructure away (for example a `continue` inside a non-final `switch` case). Dafny supports `continue` natively, so the compiler now emits it directly — the rejection was a leftover stub from before the current control-flow handling, not a real limitation of either backend. ([details](https://github.com/midspiral/LemmaScript/pull/161))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Improvement: Sped up continuous integration by caching the Dafny installation between runs and sharding verification of the example suite across parallel jobs, so the growing corpus of verified examples stays fast to check on every change. ([details](https://github.com/midspiral/LemmaScript/pull/163))
- **2026-07-11** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Documentation: Added new verified examples: a ZigZag integer-encoding module (the trick Protocol Buffers uses to store signed integers) with round-trip laws proven in both directions — establishing encode/decode as a machine-checked bijection — and an expansion of the auction example into a genuine sealed-bid second-price (Vickrey) auction with winner selection and price invariants proven. ([details](https://github.com/midspiral/LemmaScript/commit/4580ce8326ae13f2bdb6906a4a7e6a6de78ec029))
- **2026-07-11** · [flue-lemmascript](https://github.com/midspiral/flue-lemmascript) · Case Study: Launched flue-lemmascript, a case study verifying parts of a real agent-harness codebase in place. The first result: a shipped backward-scan function that counts consecutive retryable model errors was verified byte-identical — no rewrites — and proven equal to a clean recursive specification of its behavior, not merely bounds-safe. The proof exercises strict index checking, union discriminant matching, and a mid-loop `continue` together. ([details](https://github.com/midspiral/flue-lemmascript/commit/68892d584bfc57bf93009f5725842cb3d8168dd1))
- **2026-07-11** · [flue-lemmascript](https://github.com/midspiral/flue-lemmascript) · Case Study: Three more in-place, byte-identical verification results in the agent-harness case study: the context-compaction defaults derivation, where the proof pins the exact input guards under which the safety clamp prevents runaway compaction (the failure its own comment warns about); the compaction gate predicates; and a session-identity invariant showing generated internal session names can never collide with the public namespace. ([details](https://github.com/midspiral/flue-lemmascript/commit/d2d89359f257c5b81679f53332829fb8a15595d5))
- **2026-07-10** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed an unsound model of string trimming: `trim()`, `trimStart()`, and `trimEnd()` were modeled as stripping only the plain space character, so proofs about trimmed input could diverge from real JavaScript (where `"\t".trim()` is empty). The model now strips the full ECMAScript whitespace set — tabs, newlines, Unicode spaces, and the byte-order mark — guarded by a regression example plus a runtime self-test confirming JavaScript agrees on all 26 stripped code points. ([details](https://github.com/midspiral/LemmaScript/pull/158))
- **2026-07-09** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed a silent miscompilation where a user-defined field named `size` (or `length`/`keys`) on a struct was rewritten into Dafny's cardinality operator, quietly verifying a different program than the one written, with no diagnostic. The rewrite is now type-directed: it applies only where the compiler has proven the access is not a real datatype field. The whole example corpus regenerates byte-identically on both backends. ([details](https://github.com/midspiral/LemmaScript/pull/157))
- **2026-07-08** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed a class of silent name-clash miscompilations where compiler-synthesized variable names could capture or shadow user-written names — for example a map-deletion helper whose internal binder collided with the user's own variable, quietly deleting nothing, or two distinct variables merging under non-injective name mangling. Generated names now go through a freshening authority with capture-avoiding renaming, guarded by a new name-clash test gauntlet verified on both backends. ([details](https://github.com/midspiral/LemmaScript/pull/153))
- **2026-07-06** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Hardened the `lsc` command-line tool: verification flags like `--time-limit` are now honored in every mode (the documented slow-file workflow silently ran without them under regeneration), a missing Dafny installation reports 'not found on PATH — verification never ran' instead of a misleading 'verification failed', and unknown or malformed flags are rejected instead of silently ignored, closing cases where a typo could green-pass on the wrong backend or with the wrong time limit. ([details](https://github.com/midspiral/LemmaScript/commit/5de4778c6e2a9fa6fef5e322f6e408c7360949aa))
- **2026-07-05** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Batch verification moved into the toolchain: `lsc check` (and `gen`/`gen-check`) with no file argument now verifies every file listed in a project's `LemmaScript-files.txt`, honoring per-entry timeouts and extra prover flags, and `lsc claimcheck` with no argument vets every listed file's plain-English contracts the same way. Projects that install the npm package get the whole project-wide verification loop with no source checkout needed. ([details](https://github.com/midspiral/LemmaScript/pull/151))
- **2026-07-05** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: One-command toolchain install: `npm install -g lemmascript` now brings the entire toolchain, with the contract-checking satellites riding along as dependencies and a new `lsc claimcheck` subcommand forwarding to them in-process. No separate installs or PATH setup, verified end to end from the public registry. ([details](https://github.com/midspiral/LemmaScript/commit/a7c7a5d116a8a5d2e0eaabb1e54b79fbc3ec4d61))
- **2026-07-05** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Improvement: Release automation is live: pushing a version tag now publishes to npm from CI and runs a sync workflow that copies the release's spec and compiler source into the agent-skills repository, tags it in lockstep, and bumps the starter kit's submodules — about twenty seconds from tag to all three repos consistent, and idempotent by construction. ([details](https://github.com/midspiral/LemmaScript/commit/9f9513ffa30be38e03f571a8c621baee9290d5d0))
- **2026-07-04** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Option narrowing now works through bare `&&`-statement guards: `x !== undefined && x.f()` — the `if`-less guard idiom — narrows `x` in the right conjunct, matching the `if` and ternary forms. Previously this shape left the optional un-narrowed and could even lift the guarded call out of the condition, running it unconditionally; the ternary rewrite agents had to reach for as a workaround is no longer needed. ([details](https://github.com/midspiral/LemmaScript/pull/150))
- **2026-07-02** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added a `//@ lean-module <name>` directive that overrides the Lean module name generated for a file, so two identically-named source files can be compiled and verified as separate Lean libraries despite Lean's flat, global module namespace. This unblocks in-place forks that duplicate a filename — for example verifying a coding agent's CLI-side copy of `compaction.ts` alongside the original. The Dafny backend is unaffected. ([details](https://github.com/midspiral/LemmaScript/pull/149))
- **2026-07-02** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: A batch of Lean-backend improvements that lets much more real-world, existing (brownfield) TypeScript compile to verified Lean — including cross-file external declarations, discriminated-union matching, `unknown` modeled as an opaque type (matching Dafny), and more array operations like `join` and `unshift`. Existing Lean case studies regenerate identically, so the additions extend what can be verified without disturbing what already did. ([details](https://github.com/midspiral/LemmaScript/pull/147))
- **2026-07-02** · [pi-lemmascript](https://github.com/midspiral/pi-lemmascript) · Case Study: The pi coding-agent case study is now proven on both backends: the context-compaction cut-point selector — including its headline guarantee that trimming old history never leaves an orphaned tool result — plus the changelog version-comparison core and the head/tail truncation helpers are all verified in Lean 4 from the same annotated TypeScript as the existing Dafny proofs. Continuous integration now re-checks the Lean proofs on every change alongside Dafny. ([details](https://github.com/midspiral/pi-lemmascript/commit/c483dd9cb9dc4f52b7dba8d10e85e35272e4e276))
- **2026-07-02** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed the Lean example suite so three committed `.lean` files (including one proof) that were missing from the build's module roots are now compiled and checked in CI, and repaired a proof that had silently broken. Previously those files lived in the repo but were never elaborated, so regressions in them could slip by unnoticed. ([details](https://github.com/midspiral/LemmaScript/commit/da41d968d1a7c397676a7786270bcf22ffd1b51a))
- **2026-07-01** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: TypeScript's `unknown` type can now be compiled to Dafny as an opaque type instead of failing or being mis-modeled. This lets more real-world code that uses `unknown` for defensive typing pass through the verifier. ([details](https://github.com/midspiral/LemmaScript/pull/146))
- **2026-07-01** · [xyflow-lemmascript](https://github.com/midspiral/xyflow-lemmascript) · Improvement: Introduced an explicit 'unknown' marker in the formal proof model for xyflow's edge-reconnection logic, replacing a loosely-typed placeholder value. This makes the underlying correctness proof more precise about which parts of the logic are genuinely unconstrained, reducing the risk of hidden assumptions in the verification. ([details](https://github.com/midspiral/xyflow-lemmascript/commit/32dccb19c25141266d0bd271f5acb0d4fa15271e))
- **2026-07-01** · [pi-lemmascript](https://github.com/midspiral/pi-lemmascript) · Fix: Corrected the formal model used in the compaction proofs so that opaque, unmodeled data fields are represented as a proper opaque type instead of being mistakenly typed as plain integers. This closes a gap where the earlier model could have let unsound reasoning slip through undetected. ([details](https://github.com/midspiral/pi-lemmascript/commit/51cb165eb9646b5ce37c7fab1cf37d8fbc04ab7f))
- **2026-06-29** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added a new type-narrowing rule for optional chaining combined with index access (e.g. `a?.[i]`), so code using this common pattern is now correctly understood by the verifier's type checker instead of being rejected or mis-typed. ([details](https://github.com/midspiral/LemmaScript/pull/144))
- **2026-06-29** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Switch statements with non-empty fallthrough cases (a case body that falls through into the next case) are now supported when compiling to Dafny, matching real JavaScript switch behavior instead of being rejected. ([details](https://github.com/midspiral/LemmaScript/pull/143))
- **2026-06-27** · [henri-lemmascript](https://github.com/midspiral/henri-lemmascript) · Documentation: Removed the design-guardrails document from the case study because it described a design direction that was never actually implemented. It was deleted to avoid misleading readers about how the project actually works. ([details](https://github.com/midspiral/henri-lemmascript/commit/92809d972e689abdc846175e9a3fc9b97a7de0fb))
- **2026-06-25** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added support for compiling array sort-by operations (sorting with a custom comparator) into verified Dafny code, so developers can use this common array pattern in code they want to prove correct. ([details](https://github.com/midspiral/LemmaScript/pull/140))
- **2026-06-25** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added support for indexing records by enum members and by string-union values, letting verified code look up object fields using enum or literal-union keys — including a working example translated to both Dafny and Lean. ([details](https://github.com/midspiral/LemmaScript/pull/139))
- **2026-06-25** · [pi-lemmascript](https://github.com/midspiral/pi-lemmascript) · Case Study: Added a formal proof for the text-replacement engine behind the coding agent's file-editing tool, showing that applying a batch of text replacements to a file preserves all the untouched content before each edit. This further demonstrates that LemmaScript's proof annotations can verify correctness of string/array manipulation code, not just control-flow safety checks. ([details](https://github.com/midspiral/pi-lemmascript/commit/64acf443a94821c5ebc8556a1241b7829a30d18e))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Object spread (`{...a, ...b}`) is now compiled by merging fields directly rather than an unsupported pattern, with the new behavior verified in both the Dafny and Lean backends. ([details](https://github.com/midspiral/LemmaScript/pull/138))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed a Dafny verification failure that only showed up on macOS for the count-bad-pairs example, and restored a previously removed example after fixing the platform-specific issue that had caused it to fail verification. ([details](https://github.com/midspiral/LemmaScript/pull/137))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed the pre-order tree traversal example so it verifies successfully on macOS, closing a gap where proofs could pass on one platform but fail on another. ([details](https://github.com/midspiral/LemmaScript/pull/136))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added support for translating JavaScript's array `unshift` (prepend an element) into verified Dafny code. ([details](https://github.com/midspiral/LemmaScript/pull/135))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed inline string-literal union types (e.g. `"a" | "b"`, not declared via a named type) so they now compile to a plain string instead of erroring, and fixed a variable-naming bug so name-collision checks correctly cover more kinds of expressions (optional chaining, nullish coalescing, lambdas, quantifiers). ([details](https://github.com/midspiral/LemmaScript/pull/134))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed a bug where two sibling for-loops that both hoist a counter variable with the same name into the same enclosing block could incorrectly collide; also fixed string-literal values assigned via nullish-coalescing defaults or inside array literals so they correctly coerce to the surrounding string-union enum type. ([details](https://github.com/midspiral/LemmaScript/pull/133))
- **2026-06-24** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Improvement: Changed how generic type parameters with an `extends` bound are handled: instead of rejecting them, the compiler now conservatively drops the bound constraint while keeping the generic parameter itself, letting more generic TypeScript code through the verifier. ([details](https://github.com/midspiral/LemmaScript/pull/132))
- **2026-06-24** · [pi-lemmascript](https://github.com/midspiral/pi-lemmascript) · Case Study: Extended proof coverage to two more parts of the real coding-agent codebase: the logic that picks the nearest supported 'thinking level' for an AI model request (proving it never silently jumps over a level that was actually available), and the head/tail text-truncation helpers used to keep tool output within line and byte limits (proving truncated output never exceeds the requested limits). Both additions show the verification approach scaling to different kinds of everyday application logic beyond the original compaction example. ([details](https://github.com/midspiral/pi-lemmascript/commit/d456e8fbe1dbf54980013ad583f73a36edd1d3f5))
- **2026-06-22** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added a narrowing rule for nullish-coalescing combined with index access, so type narrowing correctly follows through expressions like `arr[i] ?? fallback`. ([details](https://github.com/midspiral/LemmaScript/pull/131))
- **2026-06-22** · [pi-lemmascript](https://github.com/midspiral/pi-lemmascript) · Case Study: Added a formal proof for the version-comparison helper used by the coding agent's changelog tooling, verifying its comparison logic behaves consistently. This continues the case study's push to cover more of the real production codebase with machine-checked correctness guarantees, not just the compaction feature. ([details](https://github.com/midspiral/pi-lemmascript/commit/47ae04e06ece192199f8f9f7d9e718fbf4424d5b))
- **2026-06-20** · [trace-solo-lemmascript](https://github.com/midspiral/trace-solo-lemmascript) · Improvement: Converted the game's frontend code from plain JavaScript to TypeScript, adding explicit types to the app's components, state, and build configuration. This makes the codebase safer to change going forward by catching a class of bugs at build time rather than when a player hits them. ([details](https://github.com/midspiral/trace-solo-lemmascript/commit/14e3e4cb2459539f9a76d3aa88ecd36386cb134d))
- **2026-06-19** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Fix: Fixed a bug where TypeScript's type checker would widen a string-literal union type down to a plain `string`, which then caused the compiler to lose track of the union and generate incorrect comparisons; the original union type is now preserved. ([details](https://github.com/midspiral/LemmaScript/pull/130))
- **2026-06-19** · [pi-lemmascript](https://github.com/midspiral/pi-lemmascript) · Case Study: Extended the formal-verification case study from the abstract agent-harness copy of the compaction logic to the actual shipped CLI's copy of the same code, proving the same 'no orphaned tool result' guarantees hold there too. Added a further proof that when a cut falls in the middle of a conversational turn, the reported turn-start index always points to a real turn boundary, closing a gap that could otherwise let history get truncated mid-turn. ([details](https://github.com/midspiral/pi-lemmascript/commit/706620e3c8eb4fc36bc4c592e350d5aca142d787))
- **2026-06-19** · [lemmascript-kit](https://github.com/midspiral/lemmascript-kit) · Documentation: Simplified the README's instructions for keeping the kit up to date, replacing a manual multi-step submodule-bumping procedure with a simple pull-and-rerun-setup.sh flow. Makes it easier for users to stay current without needing to understand git submodule internals. ([details](https://github.com/midspiral/lemmascript-kit/commit/a4f1f75cb92664092fee31660d02dc94a64680d0))
- **2026-06-18** · [anthropic-sdk-lemmascript](https://github.com/midspiral/anthropic-sdk-lemmascript) · Improvement: Changed how streamed tool-call arguments are parsed so that partial JSON is parsed lazily rather than eagerly on every incoming chunk, reducing unnecessary parsing work while a tool call is still streaming in. ([details](https://github.com/midspiral/anthropic-sdk-lemmascript/commit/65a01068857f521d27d8963152cd3e66cbe232ad))
- **2026-06-18** · [anthropic-sdk-lemmascript](https://github.com/midspiral/anthropic-sdk-lemmascript) · Feature: Added support for a new code_execution tool version, letting applications use the updated code-execution capability with its latest feature set when building agents that can run code as part of a conversation. ([details](https://github.com/midspiral/anthropic-sdk-lemmascript/commit/a3225175d067110fc0e9152ed2699540455aa4ce))
- **2026-06-18** · [quota-lemmascript](https://github.com/midspiral/quota-lemmascript) · Improvement: Corrected the placeholder domain shown in booking-page URLs to the app's real address, and added header links crediting the LemmaScript verification and linking to the project's source code. These are small polish fixes so the URLs and links users see match reality. ([details](https://github.com/midspiral/quota-lemmascript/commit/c4edbd2ba6f30b319b5cab602e3aff06d7b63b1e))
- **2026-06-18** · [lemmascript-vscode](https://github.com/midspiral/lemmascript-vscode) · Feature: Added highlighting for a new `contract` directive inside `//@` annotations, used for a natural-language statement of intent alongside the formal requires/ensures clauses. It's rendered in its own accent color so a contract's plain-English summary is visually distinct from its formal conditions. ([details](https://github.com/midspiral/lemmascript-vscode/commit/0b13633f78a66f3e2717bc18651a12ae37b0175d))
- **2026-06-18** · [lemmascript-vscode](https://github.com/midspiral/lemmascript-vscode) · Fix: Fixed a syntax-highlighting bug where an escaped quote (like `\"`) inside a string within a `//@` annotation would prematurely close the highlighted string, throwing off the coloring of everything after it on that line. Escape sequences are now recognized and consumed correctly, with new test cases added to guard against the regression. ([details](https://github.com/midspiral/lemmascript-vscode/commit/717d857a1fcb912c9ee554cbfd9640ba43d49f8e))
- **2026-06-18** · [lemmascript-claimcheck](https://github.com/midspiral/lemmascript-claimcheck) · Fix: Fixed a broken build caused by a type-definitions file that an earlier change depended on but that had never actually been committed to the repository. Restoring the missing file, along with the build configuration needed to compile it into the published package, let the tool build correctly again. ([details](https://github.com/midspiral/lemmascript-claimcheck/commit/a9be3fec85734f14730e454343622875dc8ae38a))
- **2026-06-16** · [LemmaScript](https://github.com/midspiral/LemmaScript) · Feature: Added a new `//@ contract` comment annotation that lets developers attach a natural-language description of a function's intent alongside its formal spec. The description isn't checked by the prover itself, but external tools (like the companion project lemmascript-claimcheck) can read it to check that the plain-English description still matches the formal requires/ensures clauses. ([details](https://github.com/midspiral/LemmaScript/pull/129))
- **2026-06-16** · [henri-lemmascript](https://github.com/midspiral/henri-lemmascript) · Improvement: Added explicit contracts (precondition/postcondition-style checks) across the edit, hooks, permissions, and transcript modules of the henri agent. This makes the assumptions each function relies on and the guarantees it provides more explicit and checkable, building on the formal verification already in place. ([details](https://github.com/midspiral/henri-lemmascript/commit/b2ce49b116aed8b846bd02d806dda88ce2ad58cc))
- **2026-06-16** · [quota-lemmascript](https://github.com/midspiral/quota-lemmascript) · Documentation: Added an auto-generated 'guarantees' report that lists every proven property of Quota's core booking logic in plain English and confirms each description actually matches its underlying formal proof. This gives a human-readable audit trail of exactly what has (and hasn't) been mathematically verified about the app's behavior. ([details](https://github.com/midspiral/quota-lemmascript/commit/0c8b2c58aebf5498838dfbeb075230c1063217d7))
- **2026-06-16** · [lemmascript-claimcheck](https://github.com/midspiral/lemmascript-claimcheck) · Feature: Introduced lemmascript-claimcheck, a new tool that checks whether a function's plain-English '//@ contract' description actually matches what its formal LemmaScript proof (its requires/ensures spec) guarantees. It works by blindly translating the formal spec back into English and comparing it to the stated intent, flagging contracts that overclaim, underclaim, or have no formal backing at all, and writes the results out as a readable 'guarantees' report per source file. ([details](https://github.com/midspiral/lemmascript-claimcheck/commit/73421f338b09db4700eff47a934f34cedefb446b))
- **2026-06-16** · [lemmascript-claimcheck](https://github.com/midspiral/lemmascript-claimcheck) · Improvement: Reworked how the tool locates its two companion command-line tools (LemmaScript's extractor and claimcheck) so it now expects them installed globally via npm by default, instead of requiring manual sibling-repository checkouts on disk. This makes the package installable and usable the normal npm way, while still allowing developers to point it at local unreleased checkouts via environment variables. ([details](https://github.com/midspiral/lemmascript-claimcheck/commit/949713c3031af14458f7c3005cda9b50f9fdc18a))
- **2026-06-16** · [quorum-lemmascript](https://github.com/midspiral/quorum-lemmascript) · Documentation: Added a plain-English 'contract' description to every formally verified function in the scheduling core, along with an auto-generated report confirming each description accurately matches its underlying formal proof. This makes it possible for someone without Dafny/proof expertise to see, function by function, exactly what has been mathematically guaranteed. ([details](https://github.com/midspiral/quorum-lemmascript/commit/9711167616eaef7f79b14ab76697b7df6771691a))

## Sitemap

- [All pages](https://lemmascript.org/sitemap.md)