An example controls statement

This example is invented. A real statement identifies its contract within seconds, so we do not publish one without its owner. The structure is the one we use.

subject
  chain         1 (Ethereum mainnet)
  address       0x1111111111111111111111111111111111111111
  block         20,000,000
  block hash    0x2222…2222
  code hash     0xabcd…ef01

statement       UPG-01, revision 3
  Only the holder of the upgrade role can change the implementation,
  and only after a delay of at least 48 hours.

verdict         proved

assumptions
  A-01  The proxy passes every other call to the implementation.
  A-02  The role holder is the contract at 0x3333…3333; how its keys
        are kept off-chain is out of scope.
  A-03  Reserves, redemptions and attestations are out of scope.

pins            model version, proof record and row, statement text hash
signature       ed25519, issuer-1, over the whole record
re-check        one command; needs read access to the tooling

Illustrative. Invented values; the signature is not real.

What each part is

Part	What it holds
Subject	The chain, the address, the block and its hash, and the hash of the deployed code. A statement is about that code at that block and nothing else
Statement	One sentence, with a revision number and a hash of its text, so two parties can be sure they mean the same claim
Verdict	Proved; refuted, with a witness (a concrete counter-example); or stated and not yet proved
Assumptions	Every assumption the verdict rests on, printed in full. Scope exclusions are printed here too
Pins	The exact versions of the model and of the proofs or scripts behind the verdict
Signature	Covers the whole record. Editing any field breaks it

What re-checking does, and does not, establish

A reviewer with access runs one command. It re-checks every cited proof, each signature, and that the verdict, the statement and the pins match the proof record. Any difference stops the run and names the cause.

The block hash, the code hash, the wording of the assumptions and the explanation attached to a witness are our signed declarations. They are not machine-checked.

Three kinds of statement

Proved or refuted in the Lean kernel. Lean is a proof assistant; its kernel is a small program that checks every step of a proof. These proofs are about a model of the contract: a precise description of its behaviour, built from code rebuilt from verified source and a snapshot of storage at one block. They are not proofs about the bytecode itself. Whether the rebuilt code matches the deployed code is a separate statement.
Configuration reads. A signed, re-runnable script reads values such as a route's required verifiers or an admin's threshold at a pinned block. No proof is involved.
Open. The statement is written down and signed, and not yet proved. Open statements are counted, never hidden.

When the facts change

block 20,150,000   watcher re-reads the facts behind 412 statements
                   1 changed: the upgrade delay is now 0 hours
withdrawn          UPG-01 rev 3   reason: delay parameter changed
standing           411 statements unchanged

Illustrative.

A withdrawn statement fails re-checking from then on. A new statement is issued for the new state, with whatever verdict the new state earns. Today this watcher is run by hand; running it continuously is planned.

We would value your view

Which control facts would you need that this leaves out?
Is "proved over a model at one block, under printed assumptions" useful evidence to you, and what would make it more so?

sam@veric.dev Book a 25-minute call