diff --git a/README.md b/README.md index 1d26690..5b7f621 100644 --- a/README.md +++ b/README.md @@ -2,8 +2,16 @@ This repository is the **git-published face** of a transparency log of formal-verification attestations: signed statements that the Lean 4 proofs -of specific cryptographic Rust libraries, at specific git commits, -re-check with exactly their documented assumptions. +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)** +the log also attests **its own accumulator machinery** — a kernel-checked +mechanization of the log's own security analysis, making this the first +deployed transparency log to carry proofs of its own honesty as one of +its own entries (subject +[`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified); +scoped to the mechanized model). Current head: tree size 13, root +`3488a2d0…`. Layout: