Skip to content

Releases: wcook04/practical-formal-verification

v0.6.2 — four first-contact changes, and a door for outside reports

Choose a tag to compare

@wcook04 wcook04 released this 17 Aug 03:26
Immutable release. Only release title and notes can be modified.
6f7d179

Release commit: 6f7d1796c72b11c079824301f880777a442ac99e

Re-cut against main. Four changes landed after v0.6.1 and the launch receipt's own check classifies all four as first-contact.

Every paper now states its publication class, whether anyone outside has reviewed it, and whether it carries a DOI — with the absence typed rather than blank. GEMINI.md and .github/copilot-instructions.md exist, because both tools look for a filename this repository did not have and fall back to guessing. The agent contract said six problems while every human surface said eight. A paper-guide test measured the day it was written rather than the property it meant to hold.

The new door

Four issue forms already exist, and all four assume you found a defect here. The most useful report this project can receive is what happened when the tool met code its author did not write — including nothing useful. transfer_report.yml asks for that, and its verdict dropdown opens with it told me nothing I did not already know and it told me something confidently wrong.

Artifacts

Wheel, sdist and SHA256SUMS.txt. Verify with shasum -a 256 -c SHA256SUMS.txt. These wheels are not byte-reproducible — a rebuild records different timestamps — so the digests describe these files, not a claim about your rebuild.

Validation

make ci: 496 passed, 2 skipped.

What this does not establish

A version number is an identity, not a claim. Every check here was still run by the author, on code the author wrote.

v0.6.1 — the tag re-cut against main

Choose a tag to compare

@wcook04 wcook04 released this 17 Aug 01:21
Immutable release. Only release title and notes can be modified.
cf6b879

Release commit: cf6b879f0003518395592f847077cdd57891d9d8

v0.6.0 was tagged earlier today. Within the hour three more changes merged, so the tag stopped describing main again. This is that tag re-cut — not new work.

What arrived after v0.6.0

Markdown tables that fit. GitHub renders a table into a fixed 1012px column with no wrap escape, so an unbreakable token — a file path, a long identifier — pushes the row off the side of the screen. Long tokens now sit in fenced code blocks, which scroll inside themselves, and scripts/check_markdown_table_render.py fails the build on a table that overflows. AGENT_ROUTES.md is an index plus per-route sections rather than one six-column grid.

Site parity distinguishes canonical from retired. A retired packet path is checked for pointing at its replacement, instead of being validated as equally canonical content.

actions/setup-python to v7. The comment beside each pin — which exists so a reader can tell what a forty-character SHA resolves to — moved with it, as did the required-tag set that keeps that comment honest. Three surfaces, not two.

Artifacts

plectis-0.6.1-py3-none-any.whl, plectis-0.6.1.tar.gz, and SHA256SUMS.txt covering both. Verify with shasum -a 256 -c SHA256SUMS.txt.

These wheels are not byte-reproducible — a rebuild produces different digests, because the archive records build timestamps. SHA256SUMS.txt is the record for these files, not a claim that anyone rebuilding will match them.

Neither distribution is on PyPI. The supported route is still the clone:

git clone https://github.com/wcook04/plectis && cd plectis

Validation

make ci at this revision: 493 passed, 2 skipped. On the merge, 17 checks green across Python 3.11–3.14, documented first contact on macOS and Ubuntu, user smoke, CodeQL.

What this does not establish

A version number is an identity, not a claim. It says which revision the description, the citation, the changelog and the artifacts agree about — not that any mechanism is correct, novel, or useful on a repository it has not seen.

v0.6.0 — the first screen says what the repository is

Choose a tag to compare

@wcook04 wcook04 released this 17 Aug 00:36
Immutable release. Only release title and notes can be modified.
7bc168d

Release commit: 7bc168d5f4fde435e15c9a0f8e48dfa54fa05f77

v0.5.0 was cut on 31 July. main moved 23 commits past it, and those commits are the ones the public description is about. This release makes the tag and the description describe the same object again.

What changed since v0.5.0

README.md opens with the seven families of mechanism the repository publishes. The local record it writes is named as the accountability layer rather than the product — it is still documented, still checked, and no longer the identity. pyproject.toml and CITATION.cff now say the same thing the README says; the package summary is what a package index publishes, and it had been describing an earlier framing.

Two guards were rewritten to check properties instead of sentences:

  • The front-door validator checks the order of the opening screen — mechanisms before record. It previously blocked three specific record-first sentences by matching them literally, which left the same framing free to arrive in different words. It had.
  • The documented no-install tour is proved against a SHA-256 map of every file in the sample project. The previous proof compared one named file to a string, and stayed green if the run had rewritten a sibling, deleted a file, or left something new behind.

Every command on the first screen now runs from a clone with no install, not only the first one — one advertised command still required a global pip install that PEP 668 refuses on the interpreter most readers have. The paper corpus is bound to the thirteen active manuscripts, with a per-problem route to the strongest checked result.

Full detail in CHANGELOG.md.

Artifacts

File Size
plectis-0.6.0-py3-none-any.whl 14 MB
plectis-0.6.0.tar.gz 18 MB
SHA256SUMS.txt digests for both

Verified from a clean virtual environment: the wheel installs and plectis --version reports plectis 0.6.0 from a directory that is not the checkout. Installed footprint is 39 MB, of which 67 MB uncompressed is packaged corpus data rather than code — the repository ships the papers and fixtures its mechanisms read.

Neither distribution is on PyPI. The supported route remains the clone:

git clone https://github.com/wcook04/plectis && cd plectis

Validation

make ci from a fresh clone at this commit: 491 passed, 2 skipped. On the merge: 17 checks green across Python 3.11–3.14, documented first contact on macOS and Ubuntu, user smoke, and CodeQL.

What this release does not establish

A version number is an identity, not a claim. It says which revision the description, the citation, the changelog and the artifacts agree about. It does not establish that any mechanism is correct, that the corpus is novel, or that the tool is useful on a repository it has not seen. Each component states its own evidence class and the authority ceiling where its result stops; the release does not raise any of them.

v0.5.0

Choose a tag to compare

@wcook04 wcook04 released this 31 Jul 04:10
Immutable release. Only release title and notes can be modified.
9539695

Plectis 0.5.0 makes the public project substantially easier to inspect from a cold clone. It adds a compact coding-agent entry, a checked paper-corpus guide with source/PDF mirrors and hashes, and a public front-door contract; it also rewrites the README around the first runnable action and preserves claim ceilings across source, install, and standalone export.\n\nThe paired Lean companion is bound to public commit b028075c6fff596143db012d6f73912f2e30f731: 992 modules, 151,761 declarations, 149,812 theorem-like declarations, and 300 principal claim links.\n\nValidation: Python 3.11–3.13 CI, smoke/timing, CodeQL, local make ci (466 passed, 2 skipped), public-site parity, and exact live hashes for all 11 hosted papers.\n\nSee CHANGELOG.md for the full release notes.

v0.4.1

Choose a tag to compare

@wcook04 wcook04 released this 26 Jul 20:52
Immutable release. Only release title and notes can be modified.
afe3760

Patch release. v0.4.0 was cut one commit before the closeout audit stopped reporting an absent tool as a detected forgery, so the latest release shipped a behaviour main had already fixed.

Fixed

  • The closeout audit no longer reports an absent tool as a detected forgery. Its pytest lane shells out to pytest, which the advertised pip install . does not provide. On a plain install the lane found nothing to run and recorded the specimen as a planted-case detection. Absence and detection are now distinct outcomes, and the lane refuses rather than inventing a verdict.
  • The public site names the pip install .[test] precondition on the cold-rerun claim, so the advertised command's exit status matches what a reader following the page literally would see.

Verifying

The four-planted-case command needs the test extra:

pip install .[test]

A plain install leaves that lane nothing to run, and it will now say so instead of reporting a detection.

Full Changelog: v0.4.0...v0.4.1

v0.4.0

Choose a tag to compare

@wcook04 wcook04 released this 26 Jul 14:54
Immutable release. Only release title and notes can be modified.
1089de1

Plectis v0.4.0 makes a public open question inspectable before an expert answer is known.

  • plectis hypothesis-handoff validates and renders a source-linked declared gap, a tentative project prior, serious alternatives, outcome-to-hypothesis discriminators, and an exact expert request.
  • Every return names repository-relative landing targets and release checks; no expert answer changes claim status automatically.
  • The worked packet asks whether evaluator-selected cases would expose a different failure profile from the author-selected fixtures.
  • The public-system paper now explains why exposing a prior and update rule makes disagreement cheaper without turning that prior into evidence. Its searchable corpus and reader-facing 20-page PDF are refreshed.
  • The exact release commit passed 456 tests (2 skipped), source smoke, installed-package smoke, Python 3.11/3.12/3.13 CI, user smoke/timing, and CodeQL.

Full details are in CHANGELOG.md and HYPOTHESIS_HANDOFF.md.

v0.3.2

Choose a tag to compare

@wcook04 wcook04 released this 26 Jul 13:11
Immutable release. Only release title and notes can be modified.
45298a2

Plectis v0.3.2 restores the advertised command-line closeout-faithfulness audit.

  • The CLI now passes the semantic negative-case evaluator through to the audit kernel.
  • All four planted forgery cases are detected by name.
  • The dedicated regression suite is part of the normal public CI floor.
  • The clean release floor passes 433 tests (7 skipped), source smoke, package-install smoke, Python 3.11/3.12/3.13 CI, user smoke/timing, and CodeQL.

Full details are in CHANGELOG.md.

v0.3.1

Choose a tag to compare

@wcook04 wcook04 released this 20 Jul 17:55
Immutable release. Only release title and notes can be modified.
906544d

A patch release for two things a stranger would have hit.

A shallow clone stopped accusing the paper

git clone --depth 1 followed by make ci produced five failures naming worked-example, Lean-file-count and receipt-flow "drift". None of them mentioned the clone.

The public-system paper pins its evidence to a specific commit, and the checks read the repository as it stood there. A truncated clone does not contain that commit, so those comparisons ran against absent data — not against anything that had actually changed. The honest reading of the output was "the paper's numbers are wrong", which was false.

The history dependency is kept deliberately. The paper makes claims about a particular past commit; re-deriving them from a receipt that same commit produced would only check that file against itself. What changed is that absence is now reported as absence — the checker names the shallow clone and the fetch that resolves it, and the checks needing the pinned commit skip with that reason instead of failing as drift.

clone before after
--depth 1 5 failed 5 skipped, 0 failed
full passing unchanged, 0 skipped

One publication owner for the site

.github/workflows/pages.yml is deleted. GitHub Pages serves this site from the gh-pages branch builder; that workflow checked out the same branch and deployed the same tree again as an artifact to the same environment, so which one won depended on which ran last.

It had already taken the published site down once — an earlier version copied a hardcoded list of files, and all three papers plus .well-known/security.txt returned 404 until it was switched off. It was disabled rather than deleted, which left the second owner one toggle away. A test now asserts no workflow deploys Pages while the branch builder owns publication.

Verification

  • make ci green on a fresh full clone of main; CI green on Python 3.11 / 3.12 / 3.13, plus CodeQL and the smoke job
  • --depth 1 clone: 5 skips, 0 failures
  • live site checked after the change: /, /.well-known/security.txt and all three papers return 200, Pages still build_type: legacy from gh-pages

On v0.3.0

v0.3.0 is unchanged and stays exactly as published. Immutable releases were enabled on this repository after it was cut, and enabling them is not retroactive — the API still reports immutable: false for it. So an immutable release could only be a new one, and this is it. No previously published artifact was moved, rewritten, or deleted.

v0.3.0

Choose a tag to compare

@wcook04 wcook04 released this 20 Jul 02:54
69e1b5a

The declared version had been 0.2.0 since 11 July while main moved 105 commits past that tag, and the v0.2.0 tag was never given a release — so the newest release anyone could see was v0.1.0 from 25 June. This release makes the version name the tree again.

What is in it

Everything merged since v0.2.0 (2026-07-11). The bulk of it is the public-system paper, which went through its sixth, seventh, eighth and ninth passes: grounding borrowed claims in primary sources, stating the contribution as a claim–evidence–limit contract rather than a ladder, placing that contract beside assurance cases and CAE notation, and bounding what it says about correctness, authorship and record repair. Alongside that: the served page is called Plectis rather than the project's former name, the README opens on the one-system-two-demonstrations frame, and CI was repaired and made considerably faster.

The full list is in CHANGELOG.md.

Verification

make ci on a fresh unauthenticated clone of this tag: 426 passed, 2 skipped. The package smoke reports version: plectis 0.3.0 on both the served and packaged paths.

What this is not

A hosted product, and not the private system. Plectis is the runnable public slice — real components packaged so you can run them locally and check what each one claims. Authority ceilings are explicit and the gates fail closed.

Plectis v0.1.0

Choose a tag to compare

@wcook04 wcook04 released this 25 Jun 17:17

Plectis v0.1.0 binds the public clone/run path to CI-backed onboarding evidence.\n\nValidation:\n- CI run 28187654563 passed on Python 3.11, 3.12, and 3.13.\n- The user-smoke/timing job passed and uploaded the onboarding benchmark artifact.\n- Fresh public clone benchmark for b76fa19: clone 2.452s, bootstrap 0.878s, smoke 2.899s, install 14.815s, installed tour 1.257s, total 22.591s.\n\nSupported first-user path: Python 3.11+ with a POSIX shell, ./bootstrap.sh, then make smoke. Windows users should use WSL until native Windows CI exists.