saymrwulf/lean-transparency-log
1
0
Fork 0
mirror of https://github.com/saymrwulf/lean-transparency-log.git synced 2026-09-04 20:03:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
lean-transparency-log/README.md
mrwulf 3d7c125789 entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed 
Six new leaves (tree 13 -> 19, root 7ee23940…):

  [13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
          certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
          generation recorded 16). The delta is the P0-P2 hardening
          campaign: scalar statements bound, kernel-side axiom gate,
          driver surface with cones, declaration coverage both directions,
          the accounting identity.
  [17]    ltl-accumulator-verified — 61 certificates; the log again carries
          proofs of its own Merkle machinery, at the hardened state.
  [18]    fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
          over the SLH-DSA-SHA2-128s verify path, apex
          fips205.slh_verify_128s_accepts_iff.

Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.

Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.

Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 17:11:59 +02:00

3.8 KiB
Raw Blame History

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 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 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 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 (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 — this README deliberately names no tree size, so it cannot go stale.

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 Ed25519 public key — the REQUIRED identity anchor; each statement's truth additionally rests on the assumptions stated in its leaf
provider.slhdsa.pub the provider's SLH-DSA-SHA2-128s public key (FIPS 205) — checks the ADDITIVE post-quantum head signature; needs OpenSSL >= 3.5, and verify.py degrades honestly below that
verify.py standalone verifier (Python stdlib + the openssl binary; fails closed without them; --all covers every published receipt)
verify_selftest.py adversarial self-test: proves the verifier's fail-closed paths reject mutated receipts

Verify everything locally, no installation:

python3 verify.py --all
python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json

The online service (same data, live endpoints + customer documentation): https://ltl.zkdefi.org

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 commit identifies the committed git tree, not dependencies or toolchains — 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. Heads additionally carry a deterministic SLH-DSA-SHA2-128s signature over the same payload: additive, so Ed25519 remains the signature a consumer must check, and honest about scope — the estate's certificates cover the verification path of both algorithms; no signing operation is proven for either, and leaves themselves are Ed25519-signed at issuance only. Heads published before 2026-08 have no SLH-DSA signature and verify.py reports them as slh_dsa:ABSENT, which is allowed — an append-only log keeps its history.