What we've shipped.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Added support for translating JavaScript's array unshift (prepend an element) into verified Dafny code.

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).

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.

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.

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.

Added a narrowing rule for nullish-coalescing combined with index access, so type narrowing correctly follows through expressions like arr[i] ?? fallback.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

The star-count diffing logic (computing per-repo deltas, splitting them into gainers/losers/unchanged, and totaling them) now has its plain-English contract claims independently checked against the formal Dafny specs backing them via LemmaScript's claimcheck tool. All five contracts — for computing diffs, extracting increases, extracting decreases, decomposing results, and extracting unchanged rows — were confirmed to accurately describe their underlying formal guarantees, with zero disputes or gaps, and the generated report is now checked into the repo as a transparency artifact.

Ran an automated tool that reads each proven function and writes a plain-English description of exactly what it guarantees, producing a human-readable report of the app's verified claims. In the process it also surfaced that one function's stated guarantee didn't actually promise anything useful, flagging it for future cleanup.

Added a machine-checked "claimcheck" report that verifies the plain-English description of the equalization function actually matches its formal mathematical specification. This gives readers a trustworthy, human-readable explanation of what the verified code guarantees, backed by an automated check rather than just a code comment.

Added a one-command setup script (setup.sh) that initializes the kit's submodules, installs the LemmaScript verifier's dependencies, and builds its CLI, along with a full README covering installation and the annotate-generate-verify workflow. This turns the repo from a bare pair of git submodules into a usable, documented starter kit for trying out LemmaScript's TypeScript-to-Dafny/Lean verification.

Removed references to retired models from the SDK's type definitions, so developers no longer see model names in autocomplete or type checks that are no longer available to call.

Launched the LemmaScript VS Code extension, which adds syntax highlighting inside the //@ specification comments (requires, ensures, invariant, decreases, and similar directives) that LemmaScript compiles to Dafny for formal verification. It layers on top of VS Code's built-in TypeScript support — regular code, IntelliSense, and type-checking are untouched — and gives each directive its own themeable color so contracts read as a distinct spec language instead of grey comment text.

Fixed a couple of small inaccuracies left over from an example project: the lemmascript skill's description still mentioned a specific past domain model ("Quorum") that no longer applied generally, and an example file path pointed one directory level too high. Both are corrected so the skill's description and example link are accurate for any project.

The compiler now preserves and exports each parameter's original default value from the source TypeScript, so tools that consume LemmaScript's intermediate representation have access to the real default expressions instead of losing that information.

The compiler now exports the original TypeScript parameter list as part of its output, giving downstream tools access to accurate parameter information rather than a lowered/transformed version.

The compiler now tracks which functions are actually part of a module's public export surface (covering inline exports, export {} lists, and re-exports). This lets downstream consumers, such as verification-boundary tooling, wrap only a module's real public API rather than its internal helper functions.

Clarified the lemmascript skill's guidance on the //@ verify annotation, spelling out that it should be left out entirely when verifying a whole new (greenfield) file, and only added selectively when retrofitting verification onto specific functions in an existing (brownfield) codebase. This removes ambiguity that could lead someone to mis-annotate a fresh project.

Updated the bundled LemmaScript language specification to its latest version, adding several new verification capabilities: an autohavoc mode that lets a function be verified even when it mixes provable logic with unmodellable framework/I-O code, a permutation predicate for reasoning about reordered arrays, support for naming external (contracted) functions with dotted names, an if-and-only-if operator, and support for more built-in array/string methods and a JSON-summary CLI command. It also narrows the async/await limitation so that async functions with no actual await can now be verified.

Fixed the order in which spread properties are merged during object spread so it correctly matches JavaScript's left-to-right, later-wins semantics.

Fixed a batch of soundness issues found during an internal audit, including how discriminated-union fallthrough control flow, nested array push operations, building a set from an array with de-duplication, and template-string concatenation are translated — with new example programs added and verified in both Dafny and Lean.

Fixed how the Lean backend wraps method receivers inside if and let expressions, correcting generated Lean code that could otherwise be malformed or unsound.

Fixed a bug where calling a function with multiple arguments could silently drop some of them during compilation to Dafny or Lean, which could produce incorrect generated code.

Fixed a soundness bug in how string comparisons (like < and >) are translated to Dafny: Dafny compares strings as raw character sequences, not lexicographically the way JavaScript does, and the generated code now accounts for that difference.

Fixed the translation of the remainder/modulo operator (%) so its behavior in generated Dafny and Lean code matches JavaScript's actual remainder semantics, which differ from the target languages' native operators for negative operands.

Fixed operator associativity in the Lean backend so expressions with chained operators are grouped the same way in generated Lean as they are in the original TypeScript.

Fixed a soundness gap found during an internal audit where type narrowing didn't correctly account for truthiness conditions, which could have let unsound proofs slip through.

Fixed incorrectly generated nested logical-implication expressions in the Lean backend and fixed how string literals in specs are escaped, both found during an internal correctness audit.

Added support for the logical "if and only if" (iff, written <==>) operator in formal spec annotations, with a new example verified in both Dafny and Lean.

Fixed how the app's date logic determines leap years and days-in-month so the math matches JavaScript's actual runtime behavior instead of a differing mathematical convention. Previously the formal model used a remainder calculation that can disagree with JavaScript for certain inputs, which could have led to incorrect date calculations once the verified logic runs in the app; a dedicated JS-compatible remainder function was added and wired into the leap-year check to close that gap.

Fixed an edge case in the formal verification rules for how xyflow determines whether a connection already exists between two nodes: the proof had incorrectly treated a connection point set to an empty string differently from one left unset. The verified logic now handles both cases the same way, matching the library's actual behavior.

After pulling in upstream Hono fixes (including the IPv6 address-formatting corrections above), the LemmaScript formal-verification proofs covering the IP-restriction matcher, IP address utilities, and file-path handling were regenerated and re-verified to stay in sync with the updated implementation. This keeps the case study's correctness guarantees valid as the underlying framework code continues to evolve.

Fixed a mismatch between how the game's verified engine checked "exact division" and how JavaScript actually computes remainders for negative numbers. The formal proof and the game logic now agree on a proper JS-style remainder, so the equalization checker can't diverge from real gameplay behavior in edge cases involving negative intermediate values.

Fixed a mismatch between the app's formally verified math proofs and its actual runtime behavior: the Lean and Dafny proofs had been modeling color-wheel calculations (like hue wraparound and palette color spread) using a modulo operation that doesn't match how JavaScript's % actually behaves on negative numbers. The proofs were updated to model JavaScript's real truncating-toward-zero remainder, so the 'formally verified' guarantees now actually correspond to the code that runs in the browser.

Fixed a bug where a type imported from another file could be printed with an invalid Dafny reference (an absolute file path) instead of its plain type name; cross-file external types are now printed correctly relative to where they're used.

Added support for two new models, claude-mythos-5 and claude-fable-5, along with a fallback mechanism that automatically retries a request against a backup model when the primary model refuses to answer, including a client-side fallback option for providers that don't support this on the server.

Added support for Managed Agents deployments and the ability to authenticate them using environment-variable credentials, along with new APIs for managing deployment runs, sessions, and secure credential vaults, expanding the SDK's coverage of the agent-hosting platform.

Added a missing 'frontier_llm' refusal category so that when a model declines to respond for this reason, applications can detect and handle it the same way they handle other documented refusal categories, instead of receiving an unrecognized value.

Reworked how the formally-verified logic for editing, hooks, permissions, and transcript handling is surfaced into the TypeScript implementation, so the guarantees proved in Dafny are more directly reflected in the running code. This tightens the link between the proofs and the shipped implementation, reducing the chance they drift apart.

Reworked how the plugin's formal correctness guarantees are generated and surfaced in the shipped source, so the proof statements backing the 'no violation is ever missed, and this beats simple one-hop checks' claims line up cleanly with the TypeScript file distributed to users. No linting behavior changed for end users; this was packaging/tooling groundwork released as version 0.1.1.

Reworked the core "can these two hands be equalized?" guarantee so it's stated as two separate, explicit soundness and completeness conditions instead of one combined rule, matching the same clearer structure already used for the game's other main proof. This makes the underlying mathematical guarantee easier to audit and sets up more precise automated verification reporting.

Extended JavaScript's "truthiness" semantics support to the Lean backend, adding narrowing and a new verified example so conditions like if (x) behave consistently whether compiling to Dafny or Lean.

Fixed how type narrowing interacts with truthiness checks (e.g. if (x) should narrow x appropriately), closing a gap where the two features could previously produce inconsistent or unsound results together.

Fixed how JavaScript truthiness is translated for arrays and numbers: arrays are always truthy in JS even when empty, and the previous translation incorrectly checked array length; this and the ! (not) operator on numbers/arrays are now translated faithfully.

Fixed how numeric truthiness is coerced to boolean: the compiler previously treated only positive numbers as truthy, but in JavaScript any nonzero number (including negatives) is truthy, and generated code now reflects that correctly.

Fixed a bug where the automatic JavaScript-truthiness coercion for if/while conditions wasn't being applied inside function bodies compiled as pure expressions, which could produce type-mismatched Dafny code.

Fixed the ordering in which third-party middleware runs relative to the SDK's own internal request handling across the direct client and the AWS, Bedrock, Vertex, and Foundry variants, so custom middleware behaves predictably and consistently regardless of which provider is being used.

Fixed an edge case in the formally-verified redirect-safety check where an empty redirect target could slip past validation before being trimmed. The logic now explicitly rejects empty redirect values up front, closing a gap in the open-redirect protection used when sending users back to a URL after an action like signing in.

Added a step-by-step tutorial walking through how the verified money-splitting core was built, plus extra inline explanations of key variables and logic, aimed at readers who want to understand how the proofs work rather than just use the app.

Recursive methods compiled to Dafny now automatically get a decreases clause added, which Dafny needs to prove that recursive functions actually terminate, removing a manual step developers previously had to handle themselves.

Published infisical-lemmascript, a case study formally verifying the permission-boundary glob-matching check in Infisical, a popular open-source secrets-management platform. The proof shows the guard that stops a role from delegating broader secret-path access than it holds is actually sound, and the work also uncovered and fixed a toolchain bug affecting recursive method proofs.

Added a case study demonstrating LemmaScript by formally verifying the glob-matching logic used in Infisical's CASL-based permission system with a Dafny specification, along with a CI workflow that runs the proof and a README explaining the approach.

Rewrote the project's design document to describe EvenTab as it was actually built: the product itself, exactly which financial guarantees are mathematically proven, and which parts (like currency display or link-based sharing) are intentionally left unverified and trusted as-is.

Refined the type definitions for the Managed Agents API, including marking certain fields as required and adding a couple of missing error and configuration fields, giving developers more accurate autocomplete and type-checking when working with these still-evolving APIs.

Added a logger accessible from within custom middleware, giving developers a supported way to emit structured log output as part of their middleware logic instead of reaching for console.log or a separate logging setup.

Fixed how request timeouts are measured so that time spent inside custom middleware no longer counts against a request's timeout budget. Previously the timeout clock started too early, meaning a middleware that retried a request internally could burn through its own deadline before the actual network call even began.

Fixed the order of operations in the client so that custom middleware now runs before requests are cryptographically signed, ensuring middleware can inspect or adjust a request before it's finalized rather than after, across the direct client and the cloud-provider SDK variants.

Introduced a new middleware system that lets developers hook into the request/response lifecycle to add custom logic (such as logging, retries, or modifying requests) without having to fork or monkey-patch the client, applied consistently across the direct API client as well as the AWS, Bedrock, Vertex, and Foundry SDK variants.

Replaced a slow cleanup database migration with a faster automated migration script after it caused a production incident, so self-hosted upgrades no longer risk stalling on that step.

Fixed how classes with multiple constructors are handled when compiling to Dafny, an edge case that previously wasn't handled correctly.

Fixed IPv6 formatting so the special all-zero "unspecified address" renders as the valid "::" instead of a single invalid ":" character, which previously broke round-tripping and could cause an ip-restriction rule like denyList: ['::'] to be silently registered under the wrong key. This closes a real correctness gap in IP-based access control rules, not just a cosmetic formatting issue.

Deleting a project no longer destroys it immediately — it's now soft-deleted (hidden right away) with a background queue permanently removing it afterward, reducing the chance of unrecoverable data loss from an accidental delete and making cleanup more reliable at scale.

Added a formal proof that converting a calendar day/time cell into the scheduling grid's internal slot number always lands in range and never lets two different cells collide, closing the last unverified piece of the grid's indexing logic. Also stood up an automated continuous-integration pipeline that re-checks these proofs and type-checks the app on every future change.

Resolved intermittent failures in the automated correctness-checking pipeline by rewriting one of the app's formal guarantees about participant availability. Instead of asserting a vague 'there exists a matching participant' style proof obligation, the code now names an explicit, computable pointer to that participant, which the verifier can reliably confirm instead of occasionally timing out.

Published a case study verifying a rate-limiting middleware for the Hono web framework, proving that its sliding-window request limiter can never allow the classic "double burst" exploit that affects naive fixed-window rate limiters — and explicitly demonstrating that the naive approach does leak while the verified one doesn't.

Published eslint-plugin-with-lemmascript, a case study showing LemmaScript verifying a real, published ESLint plugin that enforces architecture boundaries (e.g. "the UI must never reach the database layer"), proving its reachability check catches indirect violations that popular alternative lint rules silently miss.

In this formally-verified fork of the xyflow diagramming library, a new cycle-prevention check was added that stops users from connecting two nodes in a way that would create a loop in their flowchart. The logic comes with a mathematical proof that it never lets a cycle slip through and never blocks a legitimate connection, and a new interactive example (CycleGate) demonstrates it rejecting an attempted loop live on screen.

Fixed a bug where expanding the shorthand IPv6 "unspecified address" (::) produced 14 zero groups instead of the correct 8, because the expansion logic didn't fully account for multiple consecutive empty segments before filling in zeros. IP address expansion now returns the correct, standard 8-group representation.

Cleaned up the published package's TypeScript configuration: added missing type-resolution entries for several import subpaths (including the jwk middleware and JSX dev/runtime imports) that were previously unresolvable for consumers, and corrected router subpath type mappings to point at the right files. This fixes broken TypeScript imports for people using those specific subpaths.

Updated the security policy so vulnerability reports for the SDK are directed to Anthropic's official HackerOne bug-bounty program instead of an old third-party contact address, ensuring security researchers reach the right team.

Fixed a streaming parser bug where JSON numbers written in scientific notation (e.g. 1e10) inside a partially-streamed tool call weren't parsed correctly, which could cause incorrect or failed extraction of tool arguments while a response was still streaming in.

Built and published a new formally-verified rate-limiting middleware for the Hono web framework as a LemmaScript case study. Unlike typical fixed-window rate limiters, which can let a client sneak through roughly double the allowed number of requests by bursting across a window reset, this middleware's admission logic is mathematically proven (via Dafny) to never admit more than the configured limit within any sliding time window, closing that boundary-burst loophole entirely. The package was briefly published to npm and then pulled back, ending up documented and distributed as a working case study rather than a maintained npm package.

Launched eslint-plugin-with-lemmascript with its first rule, no-forbidden-reach, which catches architecture-boundary violations (like a UI module depending on the database) through any chain of imports, not just direct ones — closing a gap left by existing one-hop boundary linters. The rule's core logic is formally proved sound and complete using Dafny via LemmaScript, and every reported violation includes the exact import chain that caused it. The initial release also ships a README explaining the rule and a runnable example project demonstrating a 'laundered' violation that slips past simpler linters.

Extended the xyflow-lemmascript case study (a diagramming library used by React Flow) with a new verified feature: a cycle-detection gate that provably keeps a directed graph acyclic, demonstrated live in a React Flow demo that rejects connections which would create a cycle.

Added support for translating the bitwise OR operator (|) into Dafny, with a new example demonstrating the feature.

The error thrown when the bearer-auth middleware is configured without a way to check tokens previously mentioned only the "token" option, even though "verifyToken" is an equally valid way to configure it. The error message now mentions both options so developers aren't misled while debugging a misconfiguration.

Added a formally verified proof (with matching generated implementation) for Hono's IP-restriction matcher logic, the component that decides whether a request's IP address should be allowed or denied. This is part of this fork's ongoing case study applying LemmaScript's formal verification to a widely used, real-world web framework, showing that address-matching rules can be mathematically proven correct rather than relying on tests alone.

Fixed a login bug where a stale, unverified email alias could get automatically marked as verified; the stale-alias check now runs before any state changes across all three login paths, closing a window where an unverified alias could slip through as verified.

When an organization enforces single sign-on, users are no longer shown an email-verification step that didn't apply to their SSO login, smoothing out the login experience.

Published eventab-lemmascript, a case study verifying a group bill-splitting app, proving that money is never created or lost when dividing a shared tab and settling payments, even when amounts are rounded.

Added an architecture diagram to the new tutorial and published a public TODO/roadmap document, giving readers a visual overview of how the verification pieces fit together and clarifying what work is planned next.

Added a "design guardrails" document laying out rules and constraints meant to keep the henri case study's design consistent as it grew.

Users can now press Esc to interrupt the henri agent mid-response, giving them a way to stop a long or unwanted generation immediately instead of waiting for it to finish. The change works across all supported model providers.

Added conversation compaction to the henri agent, both as a manual command and an automatic trigger, so long chat histories get summarized instead of growing without bound. The compaction logic is backed by formal Dafny proofs, which were expanded further the same day to cover more of its behavior.

Added Ollama as a new supported model provider, letting the henri agent run against local models instead of only hosted ones. This gives users a way to run the agent fully offline or self-hosted.

Extended the verified core to handle a full restaurant bill end-to-end: splitting each item among the people who claimed it, adding tax and tip, and working out net balances so everyone can settle up. Every one of these steps is mathematically proven to conserve the money, and the work concluded with a runnable demo script showing it operating on a realistic example bill.

Shipped the first working version of the EvenTab app: a single-page web app where you add people and items, mark who ordered what, enter tax and tip, and see the final split plus who owes whom. It calls directly into the verified money-splitting logic and is now auto-deployed via a new GitHub Pages workflow.

Fixed a bug where the app could compute the final settlement (who pays whom) more than once for the same bill instead of exactly once, which could have produced incorrect payment instructions. The underlying specification was corrected so settlement is now guaranteed to happen a single time per tab.

Fixed an intermittent failure where one of the automated correctness checks would occasionally time out instead of completing, by restructuring how a calculation step was proven. The check now passes reliably on every run instead of flaking.

Tightened the guarantee behind the 'round each payment' feature so it now explicitly promises what each person's rounded payment will be, not just that the overall books balance. This closes a gap where a technically-passing but useless answer (e.g. everyone owing nothing) would have satisfied the old, weaker guarantee.

Added support for union types nested inside arrays, so array elements that can be one of several types are now correctly typed and verified, including support in the Lean backend.

Extended the workflow verification core with a proof that converting a flat, real-world list of workflow steps into the nested representation used by the formal proofs preserves the taint-leak verdict exactly. This closes a gap between the abstract proofs and what the actual adapter does with real input, so the safety guarantee can be trusted end-to-end rather than only for the idealized model.

Added a full tutorial document explaining how the LemmaScript verification of the Guardians safety argument works, making the proofs and why they matter approachable to readers who aren't already familiar with the codebase.

Added a step-by-step tutorial that walks through using LemmaScript on a real codebase, with the henri agent as the running example. It gives newcomers a concrete, guided path for adding formal proofs to their own projects instead of just abstract reference docs.

Added a new file-editing tool to the henri agent along with a Dafny proof establishing its correctness, and updated the tutorial and design docs to walk through it. This extends the set of agent capabilities backed by machine-checked guarantees rather than just tests.

Kicked off a new case-study project, EvenTab, a group bill-splitter built on a formally verified 'money core' rather than ordinary hand-tested code. The first version proves two guarantees for any way a bill is split: the resulting shares always add back up to the exact original amount, and no one is shorted or overcharged by more than a chosen rounding amount.

Introduced "autohavoc," a new feature that automatically abstracts away (havocs) the effects of code the verifier can't model, such as unmodeled external calls, so those parts don't silently produce unsound proofs; follow-up work made the reporting of what was havoced clearer and more thorough.

Fixed a bug affecting lowered/desugared assignment expressions that have no assignment target, avoiding incorrect generated Dafny in that edge case.

Privileged Access Management sessions can no longer outlive the access grant that authorized them — session duration is now capped to the grant's remaining lifetime, and expired sessions are properly cleaned up, preventing access from lingering past when it should have ended.

Added support for the new claude-opus-4-8 model along with the ability to send system instructions partway through a conversation (not just at the start) and more detailed output-token usage reporting, giving developers finer visibility into how their token budget is being spent.

Fixed the beta streaming client so that encrypted metadata attached to context-compaction events is carried through correctly. Without this fix, applications using streaming responses would silently lose data needed to maintain conversation context across a compaction boundary, even though non-streaming responses included it correctly.

Published quota-lemmascript, a verified booking app case study proving that limited-capacity slots can never be overbooked even when multiple users try to claim them concurrently, and that retrying a booking request is safe (it can't accidentally double-book).

Published a full step-by-step "Quorum" tutorial on the LemmaScript docs site walking developers through building and formally verifying a real group-scheduling app from scratch — covering design, domain modeling, running the verifier, reviewing the proof, and wiring up the UI — plus a short "hello LemmaScript" quickstart guide.

Added support for setting custom maximum file size limits when using the agent toolset, giving developers control over how large a file the built-in tools will read or write instead of being locked to a fixed default.

Fixed both the standard and beta streaming message helpers so that when a model refusal happens mid-stream, the structured refusal details (category and explanation) are preserved in the final accumulated message rather than being silently dropped, matching the behavior of non-streaming responses.

Launched Quorum, a login-free group-scheduling app in the style of when2meet, built as a tutorial project for the LemmaScript formal-verification workflow. Participants paint their availability on a shared grid and see a live heatmap highlighting the best meeting times, with the underlying scoring and export logic designed to be mathematically proven correct rather than just tested.

Launched the initial set of Claude skills for working with LemmaScript, the toolchain that lets developers write TypeScript, annotate it with lightweight verification comments, and formally prove correctness properties via a Dafny backend. The bundle includes a skill for the annotate-generate-verify workflow itself, a skill for drafting a formal design document before building a verified app, a skill for independently auditing finished proofs against that design doc, and an orientation skill for safely extending a codebase that already has a verified core.

Added a full worked example design document (for a fictional login-free scheduling app called Quorum) to the design-doc skill, showing what a proper verified-app design spec looks like end to end: the product promise, the key insight that makes verification tractable, the data model and invariants, and the staged catalog of properties to prove. This gives anyone using the design-doc skill a concrete template to model their own design documents on.

Added a perm predicate for reasoning about permutations of data (backed by a lightweight multiset model), and ported it to the Lean backend, letting developers prove that a result depends only on the multiset of some input rather than its order.

Published henri-lemmascript, a case study verifying the security- and protocol-critical core of a coding-agent CLI: its tool-permission gate (proving it can't be tricked into escaping the working directory) and its conversation-safety invariant, with the verified code imported directly by the live running agent.

Fixed skill uploads so that files nested inside a folder (e.g. "my-skill/SKILL.md") keep their directory prefix when creating a new skill version, instead of being flattened to a bare filename. Previously this made the skill-versions upload endpoint unusable, since the server requires files to live under a top-level folder and was rejecting every upload.

Launched a new case-study repo showing LemmaScript applied to "henri," a small, hackable AI agent CLI. The initial build scaffolds the CLI's tools, permission system, hooks, and model-provider support, then adds formally-verified (Dafny-backed) implementations of the permission gate, transcript handling, and hook-merging logic, along with supporting docs and a license.

Added a real backend for Quota built on Cloudflare Workers with a database, and wired the app to use it instead of only storing everything in the browser. Bookings, pages, and accounts now persist on a server, so data is no longer lost when you clear your browser or switch devices.

Replaced the placeholder sign-in flow with real email-based authentication (via Stytch magic links), so users now receive an actual email to log in rather than a simulated on-screen link. The app still falls back to the old dev-only flow when real authentication isn't configured, keeping local development simple.

Added an account settings page where signed-in users can set and edit a display name, instead of only being identified by their email address. The name is saved to the backend and shown when labeling who booked a slot on a provider's page.

Added the ability to export a booking page's confirmed reservations as a downloadable file listing each booking's slot, name, and email. Because the export reuses the same verified logic that determines seat availability, the exported data is guaranteed to match what the live page shows.

Added a step-by-step deployment guide covering how to stand up Quota's Cloudflare backend and database in production. This makes it possible for someone other than the original developer to actually deploy and run the app.

Strengthened the correctness proofs behind Quota's booking counts by proving that the number of confirmed bookings for a slot depends only on which bookings exist, not the order they were made in. This closes a gap in the formal guarantees and rules out a class of subtle bugs where reordering events could otherwise change the reported availability.

Strengthened the proof that Quorum's heatmap is order-independent so it now covers any reordering of participants' edits, not just swapping two batches at a time. This was made possible by a new 'perm' (permutation) predicate added to the underlying LemmaScript verification language specifically to express this stronger guarantee.

Updated the design doc, retrospective, README, and verification checklist to reflect the newly generalized proof that the scheduling heatmap is correct regardless of how participant edits are ordered.

Fixed a gap where a background cleanup process could remove Certificate Manager project memberships without first confirming the acting user was authorized to do so, closing a potential privilege-escalation path.

Fixed a soundness bug in how numeric division was translated, along with related fixes to how the compiler distinguishes integers from real numbers, including making the Lean backend explicitly error instead of silently emitting incorrect real-number code where it can't guarantee correctness.

Refined the formal correctness proof behind xyflow's edge-midpoint calculation so it properly models fractional division instead of assuming whole numbers, fixing a mismatch between the code's actual math and the guarantees being verified about it. This makes the verification more accurate without changing what the function returns to users.

The compress middleware gains a new contentTypeFilter option (a regular expression or a function) that lets applications decide exactly which response content types get compressed, and the underlying content-type-matching regex is now exported for reuse elsewhere. This gives developers fine-grained control over compression behavior beyond the built-in defaults.

Fixed IPv6 address formatting so a single all-zero 16-bit group is no longer incorrectly collapsed into the "::" shorthand, which per the IPv6 spec is only valid for runs of two or more consecutive zero groups. This keeps generated/normalized IPv6 addresses correct and spec-compliant.

Built and formally verified the core booking logic behind Quota, a slot-booking app: reserving a slot, cancelling, and tracking remaining capacity are all mathematically proven to never let a slot oversell and to keep seat counts accurate even after cancellations. This proof-backed foundation gives stronger correctness guarantees than ordinary testing, and everything else in the app is built on top of it.

Shipped the first working version of the Quota web app: a page where a signed-in provider can create booking pages with time slots, and visitors can view and reserve open slots through a simple console and page editor. This turns the verified booking logic into an actual usable product with a real interface.

Consolidated how accounts and sign-in work, and gave every account a unique public username (handle) derived from their email. This lays the groundwork for shareable, branded booking-page links tied to a person's own handle instead of a random ID.

Added support for TypeScript's readonly array type, letting arrays that are meant to be immutable be correctly modeled and verified.

Added support for JavaScript's typeof operator, then extended it to cover more cases, letting verified code branch on a value's runtime type the way real JavaScript does.

Added support for "opaque" types — a way to represent TypeScript types the compiler can't fully model as an abstract, un-inspectable type in Dafny and Lean, so distinct values stay distinct without unsoundly exposing their internals.

Fixed how switch statements are translated to more precisely match real JavaScript switch semantics.

Added support for string-literal union types (e.g. a type that can only be "red", "green", or "blue"), a common TypeScript pattern for representing a fixed set of allowed string values.

Added a warning when code compares two non-primitive values (objects, arrays, records) with ===/!==: the proof treats this as a structural comparison, but real JavaScript compares object identity, so the two can disagree. The compiler now flags these "equality hazards" instead of silently producing a proof that doesn't match runtime behavior.

Added support for generic type parameters on extern (foreign/native) declarations, letting external APIs with generic signatures be modeled and used from verified code.

Fixed a bug where variables hoisted out of for loops could clash in name with other variables in the same scope, which could otherwise cause incorrect generated code.

Published quorum-lemmascript, a verified group-scheduling app (similar to When2Meet), proving that the shared availability heatmap stays correct and produces the same result regardless of the order participants respond, across an optimistic, lock-free, multi-device architecture.

Published guardians-lemmascript, a case study verifying the safety guardrail behind an AI-agent workflow checker, proving that its static taint-tracking and automaton checks can never let an unsafe agent execution plan slip through undetected.

Published balanced-match-lemmascript, a case study verifying balanced-match, a small but extremely widely used (over a billion downloads a month) bracket-matching library relied on by npm and webpack, proving its core logic always finds correctly balanced pairs.

Published pi-lemmascript, a case study verifying the context-compaction logic in the "pi" AI agent harness, proving that trimming old conversation history to fit a context window can never leave a dangling tool result behind — a bug that would otherwise break the AI provider's API.

Added AGENTS.md, a reference guide aimed at AI coding agents working with LemmaScript, to the documentation site.

Added automated broken-link checking to the documentation site's build process and fixed cross-references between internal doc pages, so bad links get caught before publishing.

Launched this repo as a case study applying LemmaScript's Dafny-based verification to a real, unmodified open-source codebase: the compaction logic in the 'pi' coding agent that decides where to safely cut old conversation history. The team added in-place proof annotations (no changes to function bodies or signatures) showing the cut-point selection can never split a tool-call/tool-result pair or start the retained history on an orphaned tool result, and set up a CI workflow plus a README explaining the approach.

The static file server's path normalization only converted the first backslash in a filename to a forward slash, so multi-segment Windows-style paths like foo\bar\baz.txt ended up only partially normalized and could resolve to the wrong file or a 404. All backslashes in a path are now normalized consistently.

The Context class, previously only available as a TypeScript type, is now exported as a usable value from the main package. Developers can import it directly for things like instanceof checks or subclassing, instead of being limited to type-only references.

This repo's initial build applies LemmaScript to formally verify the core safety argument behind "Guardians" (an external agent tool-workflow safety checker by Erik Meijer): that tainted data from a source tool can never reach a sensitive sink. Machine-checked proofs, backed by a matching TypeScript implementation, cover straight-line pipelines, nested conditionals, unbounded loops, multi-source data provenance, and a security-automaton policy check. A Python-vs-TypeScript comparison harness was also added so the proofs can be checked against the real reference system rather than drifting from it.

Added formal mathematical proofs (via Dafny) covering the 2048 game engine and the session replay/recording system, replacing informal runtime checks with verified guarantees. This ensures recorded game sessions can never lose or duplicate game pieces, always follow legal moves, and can be faithfully reconstructed from a seed and action log alone, making the collected data provably trustworthy rather than just assumed correct.

Built the initial verified scheduling engine for Quorum, a login-free group-scheduling app in the style of When2Meet/Doodle. The core logic proves that the availability heatmap and 'best time' recommendation are always exactly correct, that adding availability never lowers a time slot's count, and that the result doesn't depend on the order in which people submit their availability (so concurrent, lock-free edits from multiple people always converge to the same answer).

Added the actual scheduling UI: a drag-to-paint availability grid with a live heatmap, support for creating events either as specific calendar dates or as recurring days-of-the-week, and a hover query that shows exactly who is free at a given time slot. The UI code was also migrated from JavaScript to TypeScript so it type-checks against the same verified scheduling logic it calls.

Added a real backend so Quorum events can be created, shared by link, and updated live across multiple participants' devices, instead of only working locally in one browser. It's built on Cloudflare Workers with one Durable Object per event, applying updates through the same verified scheduling logic used on the client so the server and browser can never disagree about the heatmap.

Added the project's README, explaining what Quorum is, exactly which guarantees are formally proven (versus which parts, like the UI and network layer, are simply trusted), and how to run, test, and deploy the app.

Published a retrospective on building Quorum with LemmaScript, a field report on what worked, what didn't, and where formal verification actually paid off versus where it was unnecessary overhead. It covers the reasoning behind proving only the scheduling 'answer' (the heatmap and recommendation) rather than the entire app, and how a good data abstraction let new features ship without touching any proofs.

Added a general tutorial for building verified web apps with LemmaScript, distilling the approach used in Quorum (write and prove the domain logic first, keep the UI as a thin layer over it, and use a swappable storage layer) into a reusable recipe for other projects.

Kicked off a new case study applying LemmaScript to a real, large-scale codebase by using it on VS Code itself. The initial work added formal, machine-checked specifications for core utility functions — an array search/find helper and number clamping/rotation helpers — and verified that the existing TypeScript implementations actually satisfy those specifications. A CI workflow was also added so future changes to these functions automatically re-check the proofs, and progress/candidate-function tracking docs were included to guide the next round of functions to verify.

Added a GETTING_STARTED.md walkthrough covering how to install LemmaScript and write and verify a first program, and linked it prominently from the README.

Fixed several small compilation bugs: a no-argument array .slice() copy wasn't handled, type X = number[]-style array type aliases weren't resolved correctly, and — most notably — a while loop with a single unbraced statement body (while (c) doThing();) was silently having its body dropped entirely during compilation.

Made several adjustments to how types the verifier can't fully model ("unmodeled" types) are handled during type resolution and narrowing, improving compatibility with more real-world TypeScript code.

Added an optimization that flattens lambda expressions where possible, simplifying the Dafny/Lean code generated from functional-style TypeScript.

Fixed a bug in how chained Array.isArray() checks are handled when narrowing union types.

Fixed a bug where a locally declared type could incorrectly shadow another type of the same name, causing the wrong type to be used during compilation.

Fixed a soundness bug where continue inside a C-style for loop (for (i=0; i<n; i++)) wasn't correctly re-running the loop's increment step, which could produce a proof that didn't match the real loop's behavior.

Added support for binary union types where one side is an array (e.g. T[] | U), a pattern that previously wasn't handled by the type system.

Launched trace-solo, a new platform for collecting reproducible play sessions from browser games, starting with a playable 2048 game. Every move a player makes is recorded locally and can be synced to a backend server, building a corpus of gameplay data that can later be used for training or analysis.

Added a //@ type <ty> annotation that lets developers override how a type alias is modeled by the verifier — useful for TypeScript types that can't be represented precisely, such as coercing a numeric-literal union like 5 | 15 | 30 to a plain nat.

MIME type lookups now bake the correct charset directly into each type's definition instead of guessing it from whether the type name starts with "text", so formats like SVG, XHTML, and XML also correctly get a "charset=utf-8" suffix. Extension lookups were also fixed to work whether or not a caller passes charset parameters along with the MIME type.

The compress middleware could previously send a gzip- or deflate-encoded response even when the client's Accept-Encoding header indicated it couldn't decode that encoding, which would break the client. It now properly parses Accept-Encoding (respecting quality values and wildcards) and only compresses when the client actually accepts the configured encoding.

On the Deno adapter, WebSocket upgrade responses were not echoing back the subprotocol a client requested, causing browsers such as Chrome to reject connections that asked for one. The adapter now reads the client's requested subprotocol and passes it through so the handshake completes correctly.

Responses using MessagePack content types (application/msgpack, application/x-msgpack, and +msgpack suffixes) are now recognized as compressible by the compress middleware, matching how JSON and other structured formats are already handled. This reduces bandwidth for APIs that use MessagePack for binary payloads.

Project environments (like "staging" or "production") can now be soft-deleted and restored within a grace period instead of being destroyed immediately, with a background job handling permanent cleanup afterward. The environments table also shows who deleted an environment and blocks reusing its name until the deleted one is fully purged.

Extended the balanced-match formal-verification case study with two additional proven guarantees: that whenever the algorithm returns a matched pair, the text between the delimiters is always properly balanced (no more proof-only special cases), and that the returned opening-delimiter position is always the leftmost possible match in the input string. These results, combined with the prior day's work, give strong mathematical assurance about the correctness of a function used by an enormous share of the JavaScript ecosystem.

Fixed a soundness bug in the translation of String.indexOf: the generated Dafny function previously couldn't correctly handle a negative starting index the way JavaScript does (clamping it to 0), and now carries proper bounds guarantees.

Added a new beta option that reports estimated token counts inside streamed 'thinking' blocks, so applications consuming a live response stream can track how many reasoning tokens have been produced before the model finishes.

Corrected an overclaim in the project's case-study documentation: what had been described as a proven 'conservation theorem' for the patch parser is actually a set of loop-local invariants that are never exposed as guarantees callers can rely on. The docs were rewritten to precisely describe what is and isn't proven (e.g., hunks are produced in order and every line is accounted for, but non-overlap of hunks isn't formally guaranteed), and to explain the technical reasons those properties can't currently be lifted into stronger function-level contracts.

Strengthened the formal correctness proofs behind Casbin's key-matching helpers (keyGet and keyMatch), which are used to evaluate access-control rules with wildcards. Previously the underlying string-search proof only guaranteed the position of a match was within valid bounds; now it also proves the matched substring actually equals the search pattern, closing a gap that could have let an unsound proof pass. This makes the formal verification guarantees around these security-critical matching functions stronger and more trustworthy.

Strengthened the formally-verified balance calculation at the core of this expense-splitting app: new helper functions now let the proof track the running balance after every individual expense and settlement, not just at the end, and a new check guarantees that any invalid action (like a malformed expense or settlement) leaves account balances completely unchanged. This tightens the mathematical guarantee that the app can never silently miscalculate who owes whom.

Kicked off a formal-verification case study on a fork of the widely-used balanced-match npm package (a dependency of npm, webpack, and most of the modern JS tooling stack), using the LemmaScript/Dafny toolchain to mathematically prove properties of its core bracket-matching algorithm directly on the existing TypeScript source. By the end of the day the proof covered termination and valid, correctly-ordered result indices, and culminated in a much stronger theorem showing the real algorithm behaves identically, on every possible input, to a simple reference specification, while also documenting a genuine edge case where a stricter ordering guarantee does not hold.

Added a new example implementing the Boyer-Moore majority vote algorithm, fully verified in both Dafny and Lean, demonstrating LemmaScript's ability to compile the same TypeScript source to multiple proof backends.

Merged a community contribution adding several new verified example programs (including a duplicate-detection check and a tree pre-order traversal), based on verified Dafny implementations of classic coding-interview problems.

Patched a path-traversal security bug (CVE-2026-34451) in the memory tool's directory-containment check: the old check used a plain string prefix match, so a sibling folder with a similar name (e.g. one directory named like another plus extra characters) could slip past the guard meant to keep file operations confined to the intended memory directory. The corrected check now requires an exact match or a proper path-separator boundary, and was formally verified.