From ca2a59f8a77f6a3efa0abfb5335ea0572d062e51 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 17 Aug 2026 13:27:05 +0200 Subject: [PATCH] =?UTF-8?q?site:=20the=20one=20argument=20opens=20the=20pa?= =?UTF-8?q?ge=20=E2=80=94=20three=20sentences,=20the=20dilemma=20and=20our?= =?UTF-8?q?=20point=20between?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operator order: the top value add as three sentences at the very top. S1 names the two failure modes every alternative has (cost stays with you, or belief is demanded); S2 places this site at the unique point between (proof results as cheap as one signature + a handful of hashes, without turning them into trust); S3 states the guarantee (permanently recorded, key-bound, assumption-scoped — never believed, only held accountable). The what-is-here paragraph follows concretely; the old cost paragraph is absorbed (say it once). --- provider/src/pacta_provider/webdocs.py | 29 +++++++++++++++----------- 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 056e517..f308402 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -217,19 +217,24 @@ def render_docs(log: TransparencyLog, base_path: str) -> str: · code · cv

LTL — the Lean Transparency Log

-

This site is a public notary for machine-checked proofs about cryptographic -software. A proof assistant — Lean 4, a program -that checks mathematical proofs mechanically — has verified precise statements about the code -that checks signatures: in four widely deployed Ed25519 libraries, in an -implementation of SLH-DSA (FIPS 205, the hash-based post-quantum signature -standard), and in the Merkle-tree machinery of this log itself. Every completed -proof check is recorded here as a signed, numbered entry that can never be altered or removed — -{len(entries)} entries so far, drawn live further down this page.

+

Every known way of consuming formal verification fails on one of two +sides: either the cost stays with you (re-running a theorem prover), or the cost +disappears because you are asked to believe a label. This site holds the point in +between — it makes machine-checked proof results as cheap to check as one +signature and a handful of hashes, without turning them into trust. Every claim +the operator ever makes is recorded here permanently, bound to his key, and +scoped to its exact assumptions: he can never be believed, only held +accountable.

-

Re-checking such proofs yourself takes a toolchain and real compute time. This log gives you -cheaper positions to stand on: in milliseconds you can verify that the operator is permanently -bound to every claim he ever made — and you can escalate, step by step, up to redoing -everything yourself. The ladder below lists every position, cheapest first.

+

Concretely: a proof assistant — Lean 4, a +program that checks mathematical proofs mechanically — has verified precise +statements about the code that checks signatures: in four widely deployed +Ed25519 libraries, in an implementation of SLH-DSA +(FIPS 205, the hash-based post-quantum signature standard), and in the +Merkle-tree machinery of this log itself. Each completed proof check is one +signed, numbered entry that can never be altered or removed — {len(entries)} entries +so far, drawn live further down this page. How much of our work you re-verify is +your choice, from milliseconds to everything:

Choose where you stand — the trust ladder