saymrwulf/lean-transparency-log
1
0
Fork 0
mirror of https://github.com/saymrwulf/lean-transparency-log.git synced 2026-09-03 19:53:47 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
lean-transparency-log/README.md

49 lines
2.4 KiB
Markdown
Raw Normal View History

Genesis publication: 8 leaves, 4 attested libraries, dogfood-signed head The public face of the Lean Transparency Log: every leaf (including the first run's honest audit-failure attestations), the full STH history (witness channel), per-component receipts, the provider public key, and a standalone stdlib-only verify.py. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 14:02:23 +00:00
# Lean Transparency Log — published mirror
This repository is the **git-published face** of a transparency log of
formal-verification attestations: signed statements that the Lean 4 proofs
README: log now attests its own accumulator machinery (entry 13, 2026-07-16) Broadened 'Rust libraries' framing to 'specific software'; noted the first-of-its-kind self-attestation and the current 13-leaf head. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 18:40:21 +00:00
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
verify.py fail-closed + full receipt bindings; README drops the 'honesty'/'first' overclaim (review round 10) GPT-5.6 live-site review + Fable live verification: - verify.py §4: was fail-OPEN — no openssl ⇒ signatures 'skipped' ⇒ still 'OK'. Now fail-CLOSED (exit 2 unless --structural-only, which is explicitly labelled a reduced check). --receipt was Merkle-path-only; now verifies the receipt's STH signature, key fingerprint, log_id, tree_size agreement, leaf_hash-vs-entry, and history membership before the inclusion proof. --all now also checks latest-sth == final history head and size == leaf count, and constant log_id. Adversarially tested: fail-closed exit 2; forged unsigned-root receipt REJECTED (was the 'inclusion VALID' hole); honest receipt + full run still exit 0. - README §8: I had written 'the first deployed transparency log to carry proofs of its own honesty' this session — an overclaim (the corpus proves properties of the accumulator MODEL, not operator honesty). Now: 'kernel-checked proofs about the accumulator model underlying its inclusion/consistency reasoning', 'first' softened to 'unaware of a precedent'. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 21:46:28 +00:00
mechanization of the log's security analysis, so the log carries
kernel-checked proofs *about the accumulator model* underlying its own
inclusion and consistency reasoning, as one of its own entries (subject
README: log now attests its own accumulator machinery (entry 13, 2026-07-16) Broadened 'Rust libraries' framing to 'specific software'; noted the first-of-its-kind self-attestation and the current 13-leaf head. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 18:40:21 +00:00
[`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified);
verify.py fail-closed + full receipt bindings; README drops the 'honesty'/'first' overclaim (review round 10) GPT-5.6 live-site review + Fable live verification: - verify.py §4: was fail-OPEN — no openssl ⇒ signatures 'skipped' ⇒ still 'OK'. Now fail-CLOSED (exit 2 unless --structural-only, which is explicitly labelled a reduced check). --receipt was Merkle-path-only; now verifies the receipt's STH signature, key fingerprint, log_id, tree_size agreement, leaf_hash-vs-entry, and history membership before the inclusion proof. --all now also checks latest-sth == final history head and size == leaf count, and constant log_id. Adversarially tested: fail-closed exit 2; forged unsigned-root receipt REJECTED (was the 'inclusion VALID' hole); honest receipt + full run still exit 0. - README §8: I had written 'the first deployed transparency log to carry proofs of its own honesty' this session — an overclaim (the corpus proves properties of the accumulator MODEL, not operator honesty). Now: 'kernel-checked proofs about the accumulator model underlying its inclusion/consistency reasoning', 'first' softened to 'unaware of a precedent'. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 21:46:28 +00:00
scoped to the mechanized model — it does not prove operator honesty,
signing, or execution provenance). Current head: tree size 13, root
README: log now attests its own accumulator machinery (entry 13, 2026-07-16) Broadened 'Rust libraries' framing to 'specific software'; noted the first-of-its-kind self-attestation and the current 13-leaf head. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 18:40:21 +00:00
`3488a2d0…`.
Genesis publication: 8 leaves, 4 attested libraries, dogfood-signed head The public face of the Lean Transparency Log: every leaf (including the first run's honest audit-failure attestations), the full STH history (witness channel), per-component receipts, the provider public key, and a standalone stdlib-only verify.py. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 14:02:23 +00:00
Layout:
| Path | Content |
|---|---|
| `entries/NNNNNN.json` | one log leaf per file, append-only (git history mirrors log history) |
| `entries/<component>.attestation.json` | the newest attestation per library, for convenience |
| `receipts/<component>.receipt.json` | inclusion proof binding that attestation to the latest signed head |
| `sth-history.jsonl` | **every** Signed Tree Head ever issued — the witness channel: all cloners see the same heads |
| `latest-sth.json` | the current head |
| `provider.ed25519.pub` | the provider's public key (the sole trust anchor) |
| `verify.py` | standalone verifier, Python standard library only |
Verify everything locally, no installation:
```bash
python3 verify.py --all
python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json
```
The online service (same data, live endpoints + customer documentation):
Point the online-service URL at ltl.zkdefi.org Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 17:15:03 +00:00
**https://ltl.zkdefi.org**
Genesis publication: 8 leaves, 4 attested libraries, dogfood-signed head The public face of the Lean Transparency Log: every leaf (including the first run's honest audit-failure attestations), the full STH history (witness channel), per-component receipts, the provider public key, and a standalone stdlib-only verify.py. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 14:02:23 +00:00
The provider tooling, agent tooling, and course materials:
**https://github.com/saymrwulf/proof-aware-crypto-tooling-agent**
Honesty notes, always in force: attestations cover Rust **source** at a
pinned commit (clone it — the git hash is the content hash — and build it
yourself; compilers are declared trusted base). The log deliberately
retains early leaves recording a **failed** audit run: an append-only
trust ledger keeps its history. Tree heads are signed by the merkleized,
proof-attested Ed25519 library itself, and each signature embeds the
provider's own Merkle self-check of that library's leaf.
Reference in a new issue Copy permalink