# Changes ## 0.4.8 - pin Lean 4.35.0 The Lean template pins Lean 4.35.0 in place of 4.34.1. The template records the same 34 declarations with the same statement types under both versions. Lean 4.35.0 builds the bodies of three generated `match_1` matchers differently, so their value fingerprints changed, and the template's statements are re-frozen. A project copied from the template keeps its own pin. After its `lean-toolchain` changes, the checker asks for a review and a fresh `--freeze`, as before. The checker still supports pins from Lean 4.20.0. ## 0.4.7 - an optional review of each model's properties A property can pass every check and still promise less than the code's callers rely on, and until now only the agent that wrote it read it. After writing the target table, the skill asks whether to add an independent review, one agent per target, and skips the question when the request already answers it. A headless run cannot answer, so it gets no review, and its reply says so. A reviewer follows the new review brief. It reads the source and the model's properties, assumptions and fix commits, without the modelling agent's report, and writes the bugs it expects to pass as mutations. The skill appends them to the model's mutations file and runs the mutation runner. It keeps the detected ones and gives a missed one to a new modelling agent. A finding that no mutation can express is reported as an open question. For each model, the reply says whether its properties were reviewed and how the reviewer's mutations fared. ## 0.4.6 - every Lean theorem must be breakable, past fixes become mutations, and agents' results are rechecked A Lean theorem whose hypotheses can never all hold passes whatever the code does, and the mutation runner never required a Lean theorem to fail. It now reads each Lean model's `.statements` file and prints UNCOVERED for a public theorem that no mutation makes fail, as it already did for TLA+ properties and Kani harnesses. A failing `#guard` does not count for the theorem, and private theorems are proof helpers that need no mutation. A Lean model without a `.statements` file fails before its mutations run. So does a Lean mutation with a `detects` line, which would otherwise count as covering the theorem it names. The template's `invariant_init` named the literal state `⟨0, 0⟩`, so no mutation could break it. The template now transcribes the initial state as `init`, uses it in the reach search and adds a mutation that counts an item as consumed before any claim; its statements are re-frozen. Models copied from earlier templates report `UNCOVERED theorem invariant_init` until they gain such a mutation. Step 1 lists the commits that fixed a bug in each target's code, and each brief replays them as mutations that restore the behaviour before the fix. A Kani mutation can replay a fix only in the file beside its mutations file. After the agents report, step 3 reruns every matrix, Lean check, Kani check and mutations file in the main thread and takes the verdicts from those runs. It reverts a changed property, theorem statement, statements record or Kani assumption on an existing model, or a theorem newly marked `private`, unless the row's evidence supports the change. ## 0.4.5 - follow renames before retiring a model The 0.4.4 recheck could propose retiring a model whose code still exists, and could skip the commit that changed a guarantee on purpose. Its search for the covered functions left out each model's files. A Kani harness written inside a production file, as in the bundled template, took the production functions out of the search with it, and a function renamed in place matched nothing. Step 1 now leaves out only model files that hold no production code. When a covered name is found nowhere, it finds the commit that removed the name with `git log -S` and reads all of it, and proposes retiring the model only when that commit deleted the code. The history search read a source file's first and last paths only, so a commit made at an intermediate path was skipped, and a guarantee changed there on purpose kept its old property. Step 1 now follows each source file through every rename since the sync commit and reads the log over all of its paths. ## 0.4.4 - bring existing models back in line with the code A TLA+ spec or Lean model keeps passing after the code it describes changes, because it never reads the code. When a repository already has models, the formal-verify skill now starts with them. It runs every one, finds where the functions it covers live now, and reads the commits that touched those files since the commit its header records as `Source read at`, so it follows code that moved to another file. It asks whether the model still describes the code and whether any of those commits says the guarantee changed; without that evidence the property stays, and a failure after the update is a bug candidate. Each brief has a section for an existing model: the agent edits the model's files, adds a mutation for each step the update adds, and records the commit it read the source at. When that commit is missing or no longer reachable from `HEAD`, as after a squash merge, the skill uses the last commit that touched the model. It proposes retiring a model whose functions are found nowhere and deletes it, with its CI steps and testing documentation row, when the user agrees. The reply keeps each model's verdict and adds whether it was unchanged or updated, or is proposed for retirement. A request to recheck only the existing models skips the search for new targets. ## 0.4.3 - clear the directory's credential and download-and-run holds The Claude directory held every version since 0.3.3 for a credential read and a download-and-run command, and 0.3.2 stayed the version it served. Validating the tree one deletion at a time against a throwaway repository named each trigger. The credential rule matched a parameter named for a credential in `opencode.mjs` and in the metadata test, an environment lookup in the Kani helper's `search_path` whose variable name was an argument, and the test driver writing its whole environment to a file. `search_path` now takes the inherited value, which its two callers read by name, so the assembled `PATH` and `PYTHONPATH` are unchanged; the parameters are renamed; the fake kani-driver lives in `tests/fixtures/kani-driver.py` and checks `KANI_HOME` and the loader path against `driver.json` instead of writing its environment. The download-and-run rule matched the name of Lean's evaluation command in the Lean brief, which now says to evaluate `badPairs` at top level as the template does; the command stays in the template and the checker. The CI workflow's curl of the TLC release stays and shows as a warning, which does not hold a version. The 0.3.5 notes blamed the workflow token; it was never the trigger. ## 0.4.2 - OpenCode skips stray folders and rejects incomplete skills The OpenCode plugin read every folder under `skills/` as a skill, so one folder without a `SKILL.md`, such as a scratch folder in a local checkout, failed the plugin and registered neither skill. It now skips such folders, as Pi does. A `SKILL.md` without a `name` or `description` used to register with that field undefined; the plugin now fails with the file's path and the missing field. A single-quoted `description` lost nothing but kept its quotes; it now reads as YAML does. The two bundled skills register exactly as before. ## 0.4.1 - install from npm The package is publishable to npm as `agent-formal-verify`, so Pi installs it with `pi install npm:agent-formal-verify` and OpenCode with `opencode plugin add agent-formal-verify`. A `files` allowlist limits the tarball to `opencode.mjs`, `skills/`, the license, the README and the changelog, which drops it from 77 files and 2.86 MB to 34 files and 59 kB; it leaves out the README artwork, tests, CI configuration and the Claude Code and Codex manifests. A Lean build cache under `skills/` stays out. The metadata test pins the allowlist and fails when a new root file is neither shipped nor listed as repository-only. Pushing a `v*` tag runs a workflow that checks the tag against the package version, runs the metadata tests and publishes with npm trusted publishing and provenance; it skips a version that is already on npm. The skills, the OpenCode plugin and the Git installs are unchanged. ## 0.4.0 - install in OpenCode The repository is now an OpenCode plugin for OpenCode 2.2 and later. `opencode plugin add 'git+https://github.com/michael-denyer/agent-formal-verify.git'` loads `opencode.mjs` through the package's `./server` export. It reads `skills/*/SKILL.md` and registers `setup` and `formal-verify` with their helpers, templates and references in place, and keeps any skill already registered under the same name. It has no dependencies, runs no commands and makes no network requests. The Pi package and the Claude Code and Codex plugins are unchanged. ## 0.3.5 - fetch TLC in CI without a token, and name no MCP package The CI workflow downloads the pinned TLC JAR with curl and checks it against the pinned SHA256 through the shared helper before anything runs it, instead of fetching it with the GitHub CLI under the workflow's token. The Lean brief no longer links to a Lean language-server MCP package. Neither change cleared a directory hold; 0.4.3 names the triggers. ## 0.3.4 - keep image references out of release-note code Removed the obsolete icon path from a release-note code span. The Claude directory treats bundled image paths in backticks as possible executable references, even in historical prose. The two README images added in 0.3.3 carried signed C2PA provenance manifests from the image generator; the `caBX` chunk is stripped from both, leaving the pixels unchanged, which cleared the directory's image hold. Metadata tests now reject bundled image and font paths in documentation code, reject provenance and text chunks in bundled PNGs, and guard the plugin's absence of automatic hooks and MCP or LSP servers. The README makes explicit that the plugin configures no servers or hooks and requires no credentials. ## 0.3.3 - fix only what reproduces, and name the property in the PR The skill fixes only a counter-example that shipped settings can reach, and only with a reproduction unless none is practical. When a unit test for a Lean or Kani counter-example passes on the production code, the agent corrects the model or harness, and the Lean brief permits that re-freeze. A fix PR includes any reproducing test and names the theorem, `#guard`, TLC property or Kani harness that failed. The agent uses a tool the request names and reports what it leaves unchecked. ## 0.3.2 - install in Pi The repository is now a Pi package. `package.json` points Pi at the existing `skills/` tree, so `pi install git:github.com/michael-denyer/agent-formal-verify` provides the `setup` and `formal-verify` skills with their helpers, templates and references, without a copy. The plugin test checks that the package version, license and skills path agree with the other manifests. ## 0.3.1 - name the Rust commands after the language and the tool `setup.sh rust` prepares Kani and `scripts/kani-check.sh` runs it. They replace `setup.sh bmc` and `bmc-check.sh`, and the Rust brief moves to `references/rust-brief.md`. As with TLA+ and TLC, the setup command and brief take the language's name and the scripts take the tool's. Rust mutations reject an unknown harness or an `only` line before any mutation runs. A refuted property no longer counts as a detected mutation when Kani also reports a status that the check's category does not use. ## 0.3.0 - check bounded Rust functions with Kani The Rust checker runs Kani 0.68.0 on actual functions through proof harnesses. It reports each harness's unwind bound and check count, rejects failed checks and unsatisfied cover witnesses, and prints generated concrete playback tests when available. Incomplete verification, insufficient unwinding bounds and unsatisfied covers fail. Rust mutations copy the whole crate and require detection by the named harness; compiler errors and incomplete verification do not count as detection. Setup verifies a separately installed pinned Kani bundle and invokes its verifier driver directly with the bundled toolchain. Verification and mutations use that same absolute installation, so a relative KANI_HOME or a shadowed Cargo wrapper cannot trigger Kani's automatic setup. The dependency-free bounded-queue template, setup instructions, modelling brief and CI demonstrate the Rust path. ## 0.2.8 - compare models with code and label counter-examples The Lean template prints boundary and in-range test vectors. The brief requires comparing them with the production function in its native tests before reporting that a proof describes the code, or stating that the comparison was not run. Reports label counter-examples as reproduced, reachable at shipped settings, or model-only. Lean goal and diagnostics tools remain optional. ## 0.2.7 - require reachable boundary states A TLA+ matrix can require a state with `reach |