Features / Tamper-evident ledger

Working todayProved in Lean 4

A record nobody can quietly rewrite, not even the PC's own administrator.

Every open, release and key issue joins a hash chain. Every 30 seconds it is sent to audit nodes outside the PC, run by different organizations. They refuse a rewritten past and compare their copies with each other.

30 s

between shipments to the audit nodes

About 100 to 1

ordinary edits are anchored as one Merkle root, so the record stays small

Majority

of audit nodes must hold the same history for it to count

How it works

Record, ship, compare

1

Record

Two tiers: every edit in a fine-grained chain on the PC, and the critical events plus a periodic anchor on the consortium.

  • Rebuilding the local chain cannot match anchors already sent
2

Ship

Batches are signed with the PC's root-only key. A node accepts only records that continue the chain it holds, and signs a receipt.

  • A changed past record, a gap or a bad signature is refused and alerted
  • A PC that goes silent is reported after 10 minutes
3

Compare

Nodes run by different organizations, such as ministries and an independent audit body, compare copies every few minutes. A PC that told them different stories shows up as a fork on both sides.

Not a cryptocurrency

No coins, no mining and no fees. The consortium is a fixed set of organizations that each keep a copy, so nobody, including the PC's administrator, can change the past alone.

Proven, and what is not

What the check guarantees

Proved in Lean 4

Checked on every build

  • The check accepts exactly the chains whose links and hashes hold
  • An audit node's copy stays intact and only grows
  • Two histories that pass the check and end at the same hash are the same history
Trusted, not proved

Tested and listed openly

  • A record can still be changed in the seconds before it is shipped
  • A PC kept offline ships nothing, though it is reported as silent
  • The consortium assumes most of its members are honest
  • The PC's audit key is a root-owned file, not yet in a TPM

Try it in the preview

Try it yourself

1

Run an audit node

On a second machine: zenos_auditnode.py, then enroll the PC.

2

Use the PC

Open and close sealed files. Batches arrive every 30 seconds.

3

Try to rewrite

Edit the PC's ledger. The node refuses the next batch and raises an alert.