Why a log is not a record
Observability stacks were built to debug systems, not to govern them.
Observability stacks usually answer "what did the system do?" well enough. They were never built to answer "who was authorised to do it, what did they expect, and what alternative did they reject?" Those are the questions a regulator, an auditor, or a counterparty asks after something has gone wrong. A log cannot answer them.
A log proves something ran. It cannot tell you who allowed it, what they knew, or whether the story was changed afterward.
A decision gets made. Someone writes down what happened, who approved it, and what the limit was. Months later, that written record is the only account anyone has.
Proving what happened is not the same as assigning who is to blame
Honest governance shows you the gap rather than papering over it.
A log shows that something happened. A governed record shows the recorded story behind it
- Who approved itAn authorised principal, under a declared authority and limit.
- What evidence was on fileThe evidence considered, reviewed independently, not just the agent.
- What outcome was expectedWritten down before it ran.
- The confirmation stepA one-time token was issued, then used at the moment of commit.
- A sealed fingerprintA fingerprint of the whole record. Change any single detail and it no longer matches.
| Question | Logs / Traces | OMEGA Record |
|---|---|---|
| What happened? | Event payload, timestamp, latency | Same, plus action hash |
| Who took the action? | Service / user ID | The principal named as authorised, under a declared authority and limit (P1) |
| Were they authorised at the moment of action? | Implicit in auth middleware, not in the record | A recorded freshness attestation within the declared window (P1_Freshness) |
| What evidence was considered? | Not recorded | A reasoning DAG, each node labelled fact, unknown, or declared assumption (P2, P2_DAG) |
| What alternatives were rejected? | Not recorded | Recorded when declared (P2) |
| What was the expected outcome? | Not recorded | Required (P4); environmental invariants required for trajectory commitments (P4T_EnvInvariant) |
| Can the chain be silently rewritten? | Often yes: log retention is mutable | Hash chain makes tampering detectable, unless the whole chain and its anchor are rewritten (P_ChainIntegrity) |
| Can a sub-process bypass governance by claiming "internal function"? | Frequent failure mode | Record must treat subprocess calls as decisions too. Your app enforces that; the schema documents it (P6_AtomicAgency) |
| Does a machine-checked model of the schema exist? | No | Yes: a kernel-checked Lean 4 model in the doctrine repo, establishing internal consistency of the governance properties and tamper-evidence (zero sorry, zero user axioms). It does not validate your JSON; you align records to it yourself. |
Plain facts, captured at the moment of the decision, not reconstructed from memory six weeks later.
Tamper-evidence doesn't stop someone editing a record. It means the edit can't be hidden.
A hash is a short code computed from the contents. Change anything in the record, even one digit, and the code changes completely. That code is the record's fingerprint.
Anyone can still open the file and change a number. A changed record cannot pass the check: the fingerprint recomputed from the contents will not match the one that was sealed. Anyone, anywhere, can recompute it and reach the same verdict. The evidence is in the math, not in someone's word. This holds as long as the original fingerprint is held in the chain or anchored outside the file.
Logs are necessary. They are not sufficient
OMEGA does not replace your observability stack. It sits next to it and produces the second artifact, the one a regulator can read.
A sealed fingerprint makes any later change visible. Change one detail and the seal stops matching. That part is real. What is taken on trust: that your systems actually write records like this, and that the right people are named and the right limits are set. The walkthrough shows the shape of the answer, not your live books.
So when the decision is questioned, you can show what was recorded, and prove the record is intact.
Inspect the Lean 4 proof · Read the specification · View example records