Formal Verification, OMEGA Protocol v1.4.1
v1.4.1 adds P14 Predicate Commitment as the first conjunct. Every governed record commits to the predicate version, predicate hash, attestation method, and attestation hash it satisfies.
The proof does not show that OMEGA is correct. It shows that every other governance architecture is missing something: and names exactly what.
Last checked: 25 April 2026
Proof file: OmegaV141Predicate.lean
SHA-256: ac8918ba454f22e7b00091de8d367909fd5740c258a75968666d2e0570e07b2b
Lean toolchain: Lean 4.27.0 locally
Build status: lean public/omega/formal-proof/OmegaV141Predicate.lean succeeds.
SafeVerify: pending in this workspace. SafeVerify is not installed locally; the v1.4 SafeVerify pass remains published below.
Structure: The v1.4.1 Governed predicate is a 22-conjunct bundle: P14 Predicate Commitment plus the v1.4 21-conjunct core.
Registry: Predicate ac8918ba...; attestation report 7ebc0ee0....
structure PredicateCommitment where predicate_version : String predicate_hash : String attestation_method : String attestation_hash : String def P14 (pc : PredicateCommitment) : Prop := pc.predicate_version ≠ "" ∧ pc.predicate_hash ≠ "" ∧ pc.attestation_method ≠ "" ∧ pc.attestation_hash ≠ "" def Governed := P14 pc ∧ GovernedV14Core ...
Last verified: 21 April 2026
Proof file: OmegaV14.lean
SHA-256: 15deccfcf5e314c55a33dd2254c34f988b8f71de154b154f25148c742c771302
Lean toolchain: leanprover/lean4:v4.15.0
Mathlib: not required (proof is self-contained)
Build status: lake build succeeds. No warnings from the proof file.
Kernel replay: Environment replay passed. Every declaration accepted by the Lean kernel.
SafeVerify: Ran against the compiled .olean using SafeVerify branch minif2f-kimina-check (commit 577e953). Result: exit code 0, "Finished with no errors."
Axioms: Seven representative theorems (p2_dag_necessary, p6_atomic_necessary, p1_freshness_necessary, p4t_envinvariant_necessary, all_twentyone_conjuncts_sufficient, governed_iff_all_conjuncts, authorisation_condition) each return "does not depend on any axioms". The proof uses no user axioms and none of Lean's standard axioms (propext, Quot.sound, or Classical.choice) appear on these theorems.
Sorry / placeholders: None. No sorry, no user-declared axioms.
What this verification establishes. SafeVerify confirms that the 21-conjunct formal bundle is internally consistent in Lean 4 under the standard library's three foundational axioms (propext, Quot.sound, Classical.choice). "Zero axioms" means no axioms beyond these standard foundations. "Zero sorry" means no proof obligations were deferred. The verification does not and cannot establish that the formal definitions correspond perfectly to the prose constraints they represent. This gap between specification and formalisation is a known limit of formal methods and is tracked on the adversarial methodology page as an ongoing area of review.
Structure: The Governed predicate is a 21-way conjunction representing the v1.4 primitive set: 17 conjuncts carried forward from v1.3 plus 4 new Structural Integrity constraints (P2_DAG, P6_AtomicAgency, P1_Freshness, P4T_EnvInvariant). Each new constraint closes a specific structural attack surface identified through adversarial testing on 21 April 2026.
What v1.4 closes that v1.3 does not:
· P2_DAG rejects cyclic causal graphs that pass v1.3 structural checks
· P6_AtomicAgency prevents delegation laundering through "internal subprocess" loopholes
· P1_Freshness prevents session-hijack attacks producing valid P1 records at Major and Catastrophic consequence
· P4T_EnvInvariant prevents trajectory commitments remaining "valid" while the environment shifts outside declared assumptions
What this verification establishes: The v1.4 Lean 4 formalisation is internally consistent, builds cleanly, and has been kernel-verified. Each of the four new constraints is proved necessary. The 21 conjuncts are jointly sufficient to establish the top-level Governed predicate.
What this verification does not establish: That the primitive set correctly captures all real-world governance requirements. That is an empirical claim, supported by the adversarial registry, not a formal one.
git clone https://github.com/repowazdogz-droid/omega-lean-proof cd omega-lean-proof lake build # v1.4 proof: .lake/build/lib/OmegaV14.olean # v1.3 proof: .lake/build/lib/OmegaProof.olean # Then follow SafeVerify README at: # https://github.com/GasStationManager/SafeVerify # Use branch minif2f-kimina-check for Lean 4.15 compatibility
Last verified: 21 April 2026
Proof file: OmegaProof.lean
SHA-256: 2871ed6e76473b64df394be201ef4a2eecfb50029327d334a4d58014ca1c4e64
Lean toolchain: leanprover/lean4:v4.15.0
Mathlib: not required (proof is self-contained)
Build status: lake build succeeds. No warnings from the proof file.
Kernel replay: Environment replay passed. Every declaration in the proof is accepted by the Lean kernel.
SafeVerify: Ran against the compiled .olean using SafeVerify branch minif2f-kimina-check (commit 577e953). Result: exit code 0, "Finished with no errors."
Axioms: None detected beyond Lean's built-ins. No propext, Quot.sound, or Classical.choice appear in the axiom sets of representative theorems (p1_necessary, all_governed_conjuncts_sufficient, governed_iff_all_conjuncts, authorisation_condition).
Sorry / placeholders: None. No sorry, no user-declared axioms.
Structure: The Governed predicate is a 17-way conjunction representing the v1.3 primitive set: 12 legacy primitives from v1.2 (P1-P5, P4M, P4T, P5E, P6, P6A, P6L, PCF) plus 3 new primitives (P10, P11, P12) plus 2 honest limits formalised as governance conjuncts (FAH, FAA). The honest limits are included as structural constraints to express that OMEGA does not claim accountability above the Accountability Horizon or without attestation authority integrity.
What this verification establishes: The Lean 4 formalisation of OMEGA v1.3's governance structure is internally consistent, builds cleanly, and has been kernel-verified. Every primitive is shown to be necessary (removing it produces a valid but distinct governance proposition) and the 17 conjuncts are jointly sufficient to establish the top-level Governed predicate.
What this verification does not establish: That the primitive set correctly captures all real-world governance requirements. That is an empirical claim, supported by the adversarial registry and the eight pathological worlds, not a formal one.
Repository
Source and reproduction steps: github.com/repowazdogz-droid/omega-lean-proof
git clone https://github.com/repowazdogz-droid/omega-lean-proof cd omega-lean-proof lake build # v1.4 (current): .lake/build/lib/OmegaV14.olean # v1.3 (legacy, preserved): .lake/build/lib/OmegaProof.olean # Then follow SafeVerify README: # https://github.com/GasStationManager/SafeVerify # (use branch minif2f-kimina-check for Lean 4.15 compatibility)
The proof is structured in two directions. Necessity: removing any single primitive produces a satisfiable counter-model where a distinct governance failure occurs that cannot be compensated by the remaining primitives. Sufficiency: with the full predicate-bound bundle present, no documented failure mode remains open inside the formal model.
Proof assumptions
This is a proof within a defined model of decision governance. It does not prove real-world correctness or safety. Auditability is not correctness: it is the precondition for measuring correctness.
Initial formal proof. Five primitives: P1 Governance, P2 Reasoning, P3 Traceability, P4 Expectation, P5 Confirmation. Machine-verified using SymPy on 22 March 2026. Every "Complete implies primitive" check returns UNSAT. Every "failure possible without it" check returns satisfiable. Independently verified in Lean 4 with Mathlib on 2 April 2026.
Adversarial result: Six failure modes identified in Round 1. All six closable. Three new primitives required: P4M, P5E, P6.
SymPy extended to cover P4M Materiality Binding, P5E Execution Attestation, P6 Delegation. All eight primitives necessary. All eight sufficient. Interaction tests confirm new primitives close the six specific failures the original five could not prevent.
Adversarial result: Seven failure modes identified in Round 2. Five closable. Two became honest limits: FOU (Omniscient Deceiver) and FAP (Anchor Poisoning Residual). Four new primitives required: P4T, P6A, P6L, PCF.
SymPy extended to cover P4T Trajectory Expectation, P6A Aggregate Materiality, P6L Liability Threshold, PCF Continuity-Formal. All twelve primitives necessary. All twelve sufficient. FOU and FAP confirmed to survive all twelve primitives: structurally unclosable as expected. Two additional honest limits identified in Round 3: FAB and FPS.
Round 3 conclusion: OMEGA v1.2 cannot be broken by any further protocol-level attack that does not fall into one of the six honest limit categories (full registry under v1.3).
All scripts are reproducible. The proof does not depend on any external service. Run locally with Python 3 and SymPy installed.
from sympy import symbols
from sympy.logic.boolalg import And, Not
from sympy.logic.inference import satisfiable
G, R, T, E, C = symbols('G R T E C')
Complete = And(G, R, T, E, C)
checks = {}
for prim, name in [(G,'Governance'), (R,'Reasoning'), (T,'Traceability'),
(E,'Expectation'), (C,'Confirmation')]:
no_prim = And(Complete, Not(prim))
checks[name] = {
'Complete_implies_primitive (unsat)': not satisfiable(no_prim),
'Failure_possible_without_it': satisfiable(And(Not(prim),
*[p for p in [G,R,T,E,C] if p != prim]))
}
# Result: all five NECESSARY. All five SUFFICIENT.
# Complete_implies_primitive → UNSAT for all five.
# Failure_possible_without_it → satisfiable for all five.
v1.0 result: All five primitives necessary and sufficient. Verified by Grok (xAI) via Python REPL, 22 March 2026. Independently verified in Lean 4 core, 2 April 2026. Zero errors. Zero warnings. Zero messages. Silence is the result.
import Mathlib
variable (G R T E C : Prop)
def Complete := G ∧ R ∧ T ∧ E ∧ C
theorem gov_necessary : Complete G R T E C → G := fun h => h.1
theorem rea_necessary : Complete G R T E C → R := fun h => h.2.1
theorem tra_necessary : Complete G R T E C → T := fun h => h.2.2.1
theorem exp_necessary : Complete G R T E C → E := fun h => h.2.2.2.1
theorem con_necessary : Complete G R T E C → C := fun h => h.2.2.2.2
theorem all_five_sufficient (g : G) (r : R) (t : T) (e : E) (c : C) :
Complete G R T E C := ⟨g, r, t, e, c⟩
-- Compiled silently. In formal verification, silence is the result.
from sympy import symbols, And, Not, Implies
from sympy.logic.inference import satisfiable
# Twelve primitives
P1,P2,P3,P4,P5 = symbols('P1 P2 P3 P4 P5')
P4M,P4T,P5E,P6,P6A,P6L,PCF = symbols('P4M P4T P5E P6 P6A P6L PCF')
all_twelve = [P1,P2,P3,P4,P5,P4M,P4T,P5E,P6,P6A,P6L,PCF]
Complete = And(*all_twelve)
# Failure mode symbols
F1,F2,F3,F4,F5 = symbols('F1 F2 F3 F4 F5')
F4M,F4T,F5E,F6,F6A,F6L,FCF = symbols('F4M F4T F5E F6 F6A F6L FCF')
all_failures = [F1,F2,F3,F4,F5,F4M,F4T,F5E,F6,F6A,F6L,FCF]
# Necessity check: removing any primitive allows its failure mode
necessity_results = {}
for prim, fail, name in zip(all_twelve, all_failures,
['P1','P2','P3','P4','P5','P4M','P4T','P5E','P6','P6A','P6L','PCF']):
without_prim = And(*[p for p in all_twelve if p != prim])
necessity_results[name] = {
'necessary': bool(satisfiable(And(without_prim, fail))),
}
# Sufficiency check: all twelve together block all failure modes
sufficiency = not satisfiable(And(Complete, *all_failures))
# Result:
# necessity_results → all twelve NECESSARY (each removal allows its failure)
# sufficiency → True (all twelve together block all failures)
# FOU and FAP survive: confirmed as structurally unclosable honest limits
v1.2 result: All twelve primitives necessary and sufficient. Verified in Lean 4 core: zero errors, zero warnings, zero messages. No external dependencies. Pure propositional logic. FOU and FAP survive as expected: structurally unclosable without model weight access. Two additional honest limits confirmed in Round 3: FAB (Attestation Base Integrity), FPS (Physical Staleness Gap).
Round 3 conclusion: No further protocol-level attack identified that does not reduce to one of the six honest limit categories (full registry under v1.3). The proof file is published at omegaprotocol.org/omega/formal-proof/
Three primitives added in response to two independent adversarial audits on 20 April 2026: P10 Competence Attestation, P11 Expectation Update Integrity, P12 Semantic Integrity Validation. Two additional honest limits named: FAH Accountability Horizon, FAA Attestation Authority Integrity.
Necessity: all 15 primitives required, PASS Sufficiency: conjunction internally consistent, PASS Independence: no primitive entailed by others, PASS Pair distinctness: 105 of 105 pairs distinct, PASS Triple entailment: 0 of 455 triples entail a third, PASS All-subset entailment: 0 entailments found, PASS Pathological world detection: 5 of 5 worlds detected exactly, PASS Compensation-proof: no primitive masks another, PASS Minimum violating set: 1, PASS Total checks: approximately 1,500 Total failures: 0
Repository: github.com/repowazdogz-droid/omega-lean-proof Proof file: OmegaV14.lean Structure: 21-conjunct bundle (17 v1.0 conjuncts plus 4 v1.4 structural integrity constraints) Lean toolchain: v4.15.0 Mathlib: not required Build: lake build succeeds Kernel replay: passed SafeVerify: passed (branch minif2f-kimina-check) Sorry placeholders: 0 User axioms: 0 Standard axioms on representative theorems: none See Verification Status (v1.4) section above for full details.
Repository: github.com/repowazdogz-droid/omega-lean-proof Proof file: OmegaProof.lean Structure: 17-conjunct bundle (12 v1.2 primitives + 3 new v1.3 primitives + 2 honest limits) Lean toolchain: v4.15.0 Mathlib: not required Build: lake build succeeds Kernel replay: passed SafeVerify: passed (branch minif2f-kimina-check) Sorry placeholders: 0 User axioms: 0 Standard axioms detected on representative theorems: none See Verification Status (v1.3) section above for full details.
Formal statement:
A(α) = P1 ∧ P2 ∧ P3 ∧ P4 ∧ P4M ∧ P4T ∧ P5 ∧ P5E
∧ P6 ∧ P6A ∧ P6L ∧ PCF ∧ P10 ∧ P11 ∧ P12
These failure modes cannot be closed by any pre-execution black-box governance protocol without model weight access, full execution stack verification, or deployment-layer controls as stated. They are named, owned, and published. A governance standard that does not name its limits is not a standard. It is a claim.
Agent generates a perfect compliance facade over a misaligned internal objective. Post-hoc rationalisation is indistinguishable from genuine reasoning without access to model weights or activations.
OMEGA verifies outputs and commitments, not internal cognitive fidelity. Rich structured audit records (P2 causal graphs, P4T trajectories) make deception detectable over time through systematic P4 falsification: but cannot prevent it pre-execution.
Closure requires: model weight access or formal verification of goal representations.
If the initial anchor metric for the Continuity Protocol is flawed, the protocol preserves the wrong thing. PCF prevents NLP spoofing of the evaluator: it cannot self-validate the appropriateness of the initial metric selection.
Closure requires: meta-governance at anchor definition time: external validation of metric selection independent of the governed system.
A malicious binary approved in the attestation whitelist via supply chain attack produces valid OMEGA records of invalid behaviour. P5E binds the execution payload to an approved hash: it cannot verify the semantic safety of what was approved.
Closure requires: formal verification of binary behaviour: infeasible at scale without weight-equivalent access to the binary's intent.
Physical environment changes between P5 confirmation and physical actuation. OMEGA commits what the system believed before acting. It cannot re-evaluate physical conditions at the moment of actuation: this is a fundamental boundary of pre-execution governance.
Closure requires: real-time safety interlock integration: hardware-level sensor attestation at the moment of physical execution.
OMEGA's accountability guarantees hold only for Human-Agent Collectives whose minimum compound autonomy remains below the Accountability Horizon Λ̂* = 1 − 1/|C_min|, where |C_min| is the size of the smallest mixed human-AI feedback cycle in the interaction graph. Above this threshold: proven by Tibebu (arXiv:2604.07778, April 2026): no accountability framework can simultaneously satisfy Attributability, Foreseeability Bound, Non-Vacuity, and Completeness. OMEGA is such a framework. The impossibility is structural, not an implementation gap.
Closure requires: reducing compound autonomy below Λ̂* at the deployment layer. OMEGA does not measure or constrain compound autonomy; this limit must be enforced outside the protocol.
P10 requires cryptographic binding of a competence claim to the decision record. The claim is made by an attestation authority. If that authority is compromised: through regulatory capture, credential inflation, social engineering, or collusion: a valid P10 record can accompany an incompetent agent's action. Distinct from FAB (computational attestation base), FAA covers human and institutional authority integrity.
Closure requires: deployment-layer attestation authority diversity, transparency logs for credentialing decisions, and time-bounded competence claims.
OMEGA is defined not just by what it governs: but by what it does not claim to. These limits are published alongside the proof, not hidden from it.
The mathematical proof is one line of evidence. Seven additional lines arrive independently: each from a different research direction, each confirming primitives the adversarial process identified.
Tibebu, H. (2026). The Accountability Horizon: An Impossibility Theorem for Governing Human-Agent Collectives. arXiv:2604.07778. University of Illinois at Urbana-Champaign / Responsible Intelligence Institute.
Relevance: Proves that for any Human-Agent Collective whose minimum compound autonomy exceeds Λ̂* = 1 − 1/|C_min| and which contains at least one mixed human-AI feedback cycle, no accountability framework can simultaneously satisfy Attributability, Foreseeability Bound, Non-Vacuity, and Completeness. Named in OMEGA v1.3 as honest limit FAH.
| Source | Primitive validated | How |
|---|---|---|
| SymPy + Lean 4: machine verification | All fifteen: necessary and sufficient | Formal proof. Three rounds. Every counter-model checked. Lean 4 core: zero errors, zero warnings, zero messages. Silence is the result. |
| SymPy: v1.3 extension (20 April 2026) | P10, P11, P12: necessity and sufficiency at fifteen | Extended symbolic verification; approximately 1,500 checks, zero failures. See Part 5. |
| Lean 4 (v1.4) | 21-conjunct bundle kernel-verified and SafeVerify-checked. | Zero sorry, zero user axioms, no standard axioms on representative theorems. Repository: github.com/repowazdogz-droid/omega-lean-proof (OmegaV14.lean). See Verification Status (v1.4) section for full details. |
| Lean 4 (v1.3) | 17-conjunct bundle kernel-verified and SafeVerify-checked. | Zero sorry, zero user axioms. Repository: github.com/repowazdogz-droid/omega-lean-proof. See Verification Status (v1.3) section for full details. |
| Adversarial simulation: seed 42, 10 agents | All fifteen: coverage confirmed | Every violation caught. Every gap named before closing. |
| arXiv:2603.15339: neuroscience | P1-P5 original five | Maps the five primitives to cortical column architecture independently. |
| arXiv:2506.04374: statistical physics | P5 Confirmation | Maps the Confirmation gate to a phase transition in physical systems. |
| SentinelAgent arXiv:2604.02767: April 2026 | P6 Delegation | Independently identifies delegation chains without intent verification as accountability voids. |
| Continuity paper arXiv:2604.14717: April 2026 | PCF Continuity-Formal | Independently proposes quantitative anchor baselines and deterministic rule evaluation: arriving at PCF's mechanism without knowledge of OMEGA. |
| Silent Commitment Failure arXiv:2603.21415 | P4T Trajectory Expectation | Documents systematic trajectory drift in multi-step sequences. |
| Cryptographic Binding arXiv:2603.14332 | P5E Execution Attestation | Validates the need for cryptographic binding between approved record and execution payload. |
| Composition Compliance WJAETS April 2026 | P6A Aggregate Materiality | Names the fallacy of composition in multi-agent compliance: individual compliance does not imply aggregate compliance. |
| Multi-Layer Governance WJAETS April 2026 | P6L Liability Threshold | Names the liability routing gap when high-consequence actions are delegated without threshold enforcement. |
| Live implementation: 8 domains, first external integration | All fifteen primitives: production confirmed | Deliberate Network (Alex Stojanovic), SHA-256 hashed OMEGA record returned first attempt, March 2026. |
The PCF finding is the most significant: an independent research team proposed essentially the same mechanism simultaneously. That is not confirmation: it is convergence. Two independent paths arriving at the same design is the strongest signal the design is correct.
The primitives are not a design choice. They are a discovery. The same structures appear wherever adaptive intelligence navigates uncertainty under constraint: financial markets, clinical AI, space systems, autonomous agents, biological adaptive systems. P14 adds durability across protocol versions by binding each record to the predicate it satisfied.
Any competing standard must now answer: which primitive does it remove, and which failure mode is it willing to permit?
Reproduce the proof
Primary (v1.4, current): OmegaV14.lean
git clone https://github.com/repowazdogz-droid/omega-lean-proof cd omega-lean-proof lake build # v1.4 (current): .lake/build/lib/OmegaV14.olean # v1.3 (legacy, preserved): .lake/build/lib/OmegaProof.olean
Then follow SafeVerify README at github.com/GasStationManager/SafeVerify (use branch minif2f-kimina-check for Lean 4.15 compatibility).
Legacy (v1.3, seventeen conjuncts): OmegaProof.lean
Preserved in the same repository. Superseded for current claims by the v1.4 formalisation above.
Legacy (v1.2, twelve primitives):
Available for historical reference at /omega/formal-proof/omega_v12_lean4_proof.lean
This is superseded by the v1.3 and v1.4 formalisations above.