{escape(component)}This service publishes signed attestations of formal (Lean 4) proof verification for cryptographic Rust libraries, bound into an append-only RFC 9162-style Merkle log. Customers verify a signature and a ≈{max(1, (latest.get('tree_size') or 1).bit_length())}-hash inclusion proof in milliseconds — the hours of Lean kernel re-checking happened once, on the provider's side, under memory-capped guards.
| log id | {escape(str(metadata.get('log_id', ''))[:32])}… |
|---|---|
| tree size | {latest.get('tree_size', 0)} leaves |
| latest root | {escape(str(latest.get('root_hash', ''))[:32])}… |
| root signed by | {escape(str(((latest.get('signatures') or {}).get('ed25519') or {}).get('signing_backend', 'n/a')))}
— the merkleized, proof-attested Ed25519 library itself; before signing, the provider
Merkle-verified that library's own leaf (index {provenance.get('signing_library_leaf_index', '?')},
certificates {escape(str(provenance.get('signing_library_certificates_proven', '?')))}) against this very tree |
| attested components | {len(components)} |
| component | claim document | proof of inclusion |
|---|
Each attestation names the exact git commit it covers, every certificate with its observed axiom cone, and the machine-protection used during replay. The log also retains earlier leaves that honestly record a failed audit run — an append-only trust ledger keeps its history.
GET {base}/v1/sth latest Signed Tree Head
GET {base}/v1/sth-history every head ever signed (witness material)
GET {base}/v1/sth-consistency?first=N consistency proof from your pinned size
GET {base}/v1/proof?component=NAME inclusion proof for the newest attestation
GET {base}/v1/attestation?component=NAME
GET {base}/v1/entries?start=N&end=M
GET {base}/v1/metadata log identity
GET {base}/healthz
Everything is verifiable offline. Clone the mirror repository (published on GitHub
and on this Forgejo), which contains every leaf, every signed tree head, the provider
public key, and a standalone verify.py (Python standard library only,
≈100 lines). It recomputes the entire tree from the leaves, checks every historical
head against its prefix, verifies the signatures, and checks any inclusion proof:
git clone <mirror-url>/lean-transparency-log python3 verify.py --all
For agents: the pacta tool adds pinning (split-view defense),
freshness policy, and the option to verify signatures through the
proof-attested Ed25519 code path itself
(pacta receipt-verify … --sth-store … --require-verified-verifier).
Means: the provider whose key you hold attests that the Lean proofs of the named repository at the named commit re-check with exactly the documented assumptions, and this attestation is irrevocably part of the log everyone sees.
Does not mean: a verified binary. The proofs cover Rust source; you clone the attested commit (the git hash is the content hash) and build it yourself — compiler and build remain declared trusted base until the R5 program (reproducible builds) lands. Every attestation carries the full residual-risk list; honesty about the boundary is the product.
"""