From 7c3f285f348dbebee262829de6bc65afe1925553 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 16 Aug 2026 18:32:42 +0200 Subject: [PATCH] =?UTF-8?q?docs:=20dated-record=20clarity=20for=20the=20pr?= =?UTF-8?q?e-Green=20scan=20=E2=80=94=20attestations=20that=20have=20since?= =?UTF-8?q?=20occurred=20say=20so;=20leaf-index=20numbering=20unified?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c4b593c..fa4fb4e 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ This repository is the **git-published face** of a transparency log of formal-verification attestations: signed statements that the Lean 4 proofs of specific software, at specific git commits, re-check with exactly their documented assumptions. Its first twelve leaves attest four cryptographic -Rust libraries (Ed25519 implementations); as of **entry 13 (2026-07-16)** +Rust libraries (Ed25519 implementations); as of **its thirteenth entry (leaf index 12, 2026-07-16)** the log also attests **its own accumulator machinery** — a kernel-checked mechanization of the log's security analysis, so the log carries kernel-checked proofs *about the accumulator model* underlying its own @@ -12,7 +12,7 @@ inclusion and consistency reasoning, as one of its own entries (subject [`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified); scoped to the mechanized model — it does not prove operator honesty, signing, or execution provenance). As of **2026-08** the log also attests -the **SLH-DSA (FIPS 205) verify-path proofs** +the **SLH-DSA (FIPS 205) verify-path proofs** (leaf 18) ([`fips205-slhdsa-verified`](https://github.com/saymrwulf/fips205-slhdsa-verified)) and its heads carry an **additive post-quantum SLH-DSA-SHA2-128s signature** beside the required Ed25519 one. The current head is `latest-sth.json` —