From 7cc5982af32861c9628ab6ca92c381e5bfae3da0 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 22 Aug 2026 15:18:26 +0200 Subject: [PATCH] site: the paper card finally joins the redesign MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The last fossil paragraph on the page — an ePrint-era compressed table of contents, version-patched five times, never re-read as prose. Five undefined terms of art in one 120-word sentence, a semicolon train of metadata, internal bookkeeping speaking to visitors ('the version is printed on the title page'), changelog voice ('New in the August 2026 revisions'). Now: title, clean metadata line (pages, version, DOI), and three sentences that answer the visitor's only question — should I click: the guarantees-and-non-guarantees discipline at referee depth, the sn=0 war story, and the claim matrix as the recommended entry point. New law (rule 13): fact-patches require whole-card re-reads — fact probes pass on unreadable prose. --- provider/src/pacta_provider/webdocs.py | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 57bb7b2..56344ec 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -397,21 +397,16 @@ our roadmap. (The full walk-through is lecture 11 of the Jupyter c

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log -(PDF, 25 pages, v0.15 — revised August 2026; the version is printed on the -title page; DOI 10.5281/zenodo.22057482) — the trust decomposition (expensive verification produces an -observation; transparency makes the observation accountable; consumer-local policy decides -acceptance), collision-extracting soundness for inclusion and consistency, scheme-level -accountability GAMES with an explicit composition theorem (head authenticity, position -binding, history binding with a fully proved prefix-transport induction, context-scoped -fork evidence — all discharged by named reductions), the policy boundary where -operator labels can veto but never grant acceptance, and the measured model/deployment -divergence reported as a result rather than hidden — now together with its closure: the -divergence traced to one omitted RFC 9162 conjunct (Step 7's sn = 0), -zero divergences after the one-line restoration, confirmed by a three-way regression. -New in the August 2026 revisions: the deployment evaluated to its current nineteen-leaf, dual-signed state, an -instantiation section for the SLH-DSA (FIPS 205) verify path — eleven certificates, -five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the -Ed25519 tiers.
+(PDF, 25 pages · v0.15, August 2026 · DOI +10.5281/zenodo.22057482). +The full design and its security analysis: what the log guarantees, stated as +precise games with proofs — and what it deliberately does not guarantee, with +the same honesty discipline as this page, at referee depth. It also tells the +project’s best war story: the mechanized model caught our own deployed +verifier omitting a single condition of RFC 9162 — invisible to ordinary +testing, 3,867 wrong acceptances across 73,573 adversarial cases, zero after +the one-line fix. If you read one thing, read the claim matrix at the end: +every promise, what establishes it, and what remains assumed.

Log heads are signed offline; this service is read-only and holds no