Assurance architecture · Research prototype · PROVEN

OMEGA

When an AI decision is questioned later, can you reconstruct what happened? A log shows that something ran. It does not show who approved an action above the agent's limit, what evidence was on hand, what outcome was expected, or whether the record has been changed since. OMEGA seals that record at the moment of the decision so it can be replayed and its seal rechecked.

What this establishes is narrow: the record is intact and can be reconstructed. It does not establish that the decision was right, and it does not expose the model's internal reasoning; it preserves the recorded decision context.

What this establishes

• Record integrity. An edit that does not also re-seal forces a hash mismatch.
• Chain integrity. Editing one record breaks the next record's hash link.
• Independent recomputation. Anyone can recompute the fingerprint from the JSON and reach the same verdict.
• Visible tamper detection. The check fails loudly rather than silently.

What this does not establish

• The truth of the inputs.
• The correctness of the decision.
• That the recorded reasoning is the real reasoning.
• Protection against an actor who can rewrite the whole record chain and forge its external anchor.

Trusted base

The Lean 4 model is checked by the Lean kernel (v4.27.0) and depends only on Lean's three standard axioms, propext, Classical.choice, Quot.sound, with no user-declared axiom and no Mathlib. SHA-256 is modelled as an opaque compute_hash; collision-resistance is carried as a discharged theorem hypothesis, not assumed as an axiom. Recomputation in the browser trusts the browser's own crypto.subtle implementation.

Inside a sealed record

A worked case. A support agent proposed a £4,820 refund. That is above the agent's £2,500 limit, so a manager, Sarah Okafor, approved it under Tier C escalation. The decision was sealed at that moment. The sealed record holds the five stages needed to understand or challenge the decision later: authority, evidence, expected outcome, confirmation, and traceability.

Break it yourself

Every hash below is recomputed in your browser with SHA-256 over the record's RFC 8785 canonical form, the same canonicalisation omega-demo/examples/refund-escalation.json uses. Edit the approval limit and watch the recomputed fingerprint stop matching the seal.

How the record is checked

A log shows that something ran. A replayable record shows who allowed it, the evidence at commit time, the expected outcome, the confirmation step, and whether the sealed copy was edited later. Anyone can recompute the fingerprint and see whether the stored record still matches what was committed. On its own that catches accidental edits; a deliberate editor with write access can re-seal. Chaining each record to the last, with the latest hash held outside the store, makes deliberate edits detectable.

Why a log is not a record is covered in the specification and the example record below.

The assurance architecture

OMEGA is two witnesses.

• The integrity witness seals the record. Recomputing the fingerprint shows whether the stored copy still matches what was committed, as in the demo above. It establishes integrity, not correctness.
• The evidence witness grades whether a record's evidence can be independently reconstructed, not whether it is true. Its results and grading are covered on the evidence witness page.

Result

The shipped root theorems of the Lean model are machine-checked; a fresh public clone builds green (16 jobs) and #print axioms reports 0 user-declared axioms. Tampering a sealed record forces a hash collision, the record chain is append-only, and the canonical encoding is injective and round-trips. The depth pages carry the detail:

• The specification
• The verification and its honest limits
• The replay challenge
• An example governed decision record

Reproduce

The Lean model, from a clean public clone:

git clone https://github.com/repowazdogz-droid/omega-lean-proof
cd omega-lean-proof
lake build                         # Build completed successfully (16 jobs)
lake env lean probes/AxiomProbe.lean   # 0 user-declared axioms

The record demo, locally, against the CLI:

node dist/cli.js verify examples/refund-escalation.json   # recomputed hash matches
node dist/cli.js tamper                                   # hash mismatch, exit 1

This pass. The Lean model was re-verified this pass: lake build and the axiom probe were re-run from a fresh public clone at 2fab5d1 (16 jobs, 0 user-declared axioms). The tamper demo's canonical hashes were re-computed independently and reproduce e747c3fd (intact) and b2e3c3e7 (edited). The record CLI itself was not re-run this pass (its repository is private).

Independent reproduction

None known. The Lean build and axiom audit were reproduced from a fresh public clone during the evidence inventory; that is author self-reproduction, not independent third-party reproduction. Replication is invited.

Prior art and positioning

Tamper-evident logging and hash chains (Haber and Stornetta, 1991), the trusted computing base literature, and canonical serialisation (RFC 8785). The contribution is the governed-decision record structure and the machine-checked internal-consistency and tamper-evidence properties, not the discovery of hash chaining.

Who this is for

OMEGA is not a gate or a guardrail. It does not block actions. It preserves the record needed to replay and challenge a decision later, for engineers wiring records in, researchers checking the specification and the Lean work, and auditors replaying a decision months afterwards.

Source: repowazdogz-droid/omega-lean-proof