Constraint-preserving decision systems for autonomous AI.
OMEGA treats autonomous decisions as constraint-preserving systems.
Each decision must satisfy constraints across the five foundational layers:
A governed record makes these constraints:
OMEGA defines the minimal structure required to achieve this.
The system is grounded in a dependency-ordered stack of constraints. These layers form a partially ordered constraint system, not a strict hierarchy, but lower layers constrain what higher layers can achieve.
What physics permits.
Note: Specific results such as Floyd et al. (2025), which bound classification expressivity in biochemical systems, are treated as evidence of constraint-limited decision processes in physical systems, not as direct constraints on OMEGA itself.
What can be known and recorded.
These define limits on:
A decision record must contain sufficient information to preserve its meaning. Omission is not neutral — it destroys reconstructability.
What reasoning is valid.
This is where OMEGA's formal verification work sits. OMEGA uses two independent tools: Lean 4 for the kernel-verified minimality bundle, and SymPy for three rounds of symbolic adversarial testing on the v1.0 primitive bundle. Dual-tool verification reduces the risk that a single system's implementation details are doing load-bearing work.
Proof bundle status (v1.4):
The Lean 4 bundle formalises 21 structural properties of governed records as a single Governed predicate — 17 conjuncts from v1.3 plus 4 new Structural Integrity constraints (P2_DAG, P6_AtomicAgency, P1_Freshness, P4T_EnvInvariant) added after adversarial testing on 21 April 2026.
leanprover/lean4:v4.15.0lake build succeeds with zero warningspropext, Quot.sound, and Classical.choiceminif2f-kimina-check, commit 577e953) returns exit code 0, "finished with no errors"github.com/repowazdogz-droid/omega-lean-proofEach conjunct corresponds to a specific class of failure mode. The proofs are machine-checked, externally verified, and reproducible from the public repository.
Design assertion (not a theorem):
The primitive set is constructed such that each primitive enforces at least one property that cannot be recovered by any combination of the remaining primitives. This is supported by failure-mode analysis: removing any primitive admits a distinct, uncompensable failure mode.
Without the Lean bundle, this claim is rhetorical. With it, the structural properties are machine-verified; the minimality claim itself remains a design-level statement backed by those properties.
Known limit of formalisation:
The Lean bundle verifies internal consistency of the formal definitions. It does not and cannot verify that the formal definitions correspond perfectly to the prose constraints they represent. This specification–formalisation gap is a known limit of formal methods and is tracked on the adversarial methodology page as ongoing work.
What systems can be built and composed.
OMEGA composes with the structural infrastructure now consolidating under the Linux Foundation: MCP (Model Context Protocol, 97M monthly SDK downloads by March 2026) for agent–tool access, and A2A (Agent2Agent, 150+ production implementations) for inter-agent coordination. Neither layer covers what was committed before action. P1, P3, P4, and P6 attach directly to MCP tool-call traces and A2A Task Objects.
These govern:
Predictions only hold within declared validity domains. Systems must preserve causal ordering and traceability. Correct-looking outputs are insufficient without structural guarantees.
How agents behave under rules.
These determine:
Truth does not survive unless incentives align with it. Commitments, materiality, and liability are structural, not optional. Delegation without incentive alignment creates drift.
Where the system is applied.
This layer does not constrain OMEGA's design directly. It reflects environments in which constraint-preserving decision records are required. Governance structures converge across domains when failure matters.
Decision systems involving:
face trade-offs between:
These tensions are well-documented across distributed systems theory (FLP impossibility, Byzantine fault tolerance) and accountability theory more generally.
This limit can be described as an accountability horizon: beyond a threshold of autonomy and complexity, no framework can guarantee all four properties simultaneously.
OMEGA does not resolve this limit. It is designed to:
The horizon is not currently formalised within the Lean bundle; formalisation is ongoing work.
Biological systems — cortical decision architectures and predictive processing — show similar structural patterns:
These are evidence that constraint-shaped decision systems exist in nature, not a foundation of OMEGA.
Note: OMEGA's vocabulary overlaps with predictive-processing neuroscience. This is a descriptive borrowing for clarity, not a claim that OMEGA is a neuroscientific model.
| Constraint layer | Representative primitives |
|---|---|
| Logical | P2 (reasoning), P2-DAG |
| Information | P3 (traceability), P5E (execution attestation) |
| Structural | P4T (trajectory), PCF (continuity) |
| Incentive | P4 (expectation), P6L (liability threshold) |
Primitives such as P1, P10, and P11 primarily support deployment-layer requirements and are not shown in this foundational mapping.
This is a compressed view; a full primitive-to-layer mapping is maintained separately.
Failure in OMEGA is a system producing correct-looking outputs while silently violating the conditions required for those outputs to be valid.
Specific failure classes addressed in v1.4:
Each addition was introduced after adversarial testing identified a concrete attack that the prior primitive set failed to prevent.
OMEGA's goal is not to eliminate failure. It is to make failure observable and attributable.
A decision record is valid under OMEGA if:
Outside those conditions, the system must state what it cannot guarantee.
OMEGA's formal claims are independently reproducible.
git clone https://github.com/repowazdogz-droid/omega-lean-proof cd omega-lean-proof lake build # Lean 4 v4.15.0
Outputs:
.lake/build/lib/OmegaV14.olean.lake/build/lib/OmegaProof.oleanThe compiled .olean files can be verified against SafeVerify (branch minif2f-kimina-check) for independent kernel acceptance of all declarations.
OMEGA's adversarial methodology has produced four rounds of structural attack testing: three rounds on the SymPy v1.0 bundle, one round on v1.4's structural integrity constraints. Each round identified specific failure modes. v1.4's four new primitives were introduced to close the attack surfaces identified in the fourth round. The methodology and registry are maintained as ongoing work.
OMEGA is not:
OMEGA is a structural specification with a machine-verified and externally checked property set. Its guarantees are:
Everything outside those guarantees remains an engineering, legal, or policy question.
"Constraint propagation" is not a novel concept. It is well-established in logic, artificial intelligence, and optimisation.
OMEGA does not introduce a new form of constraint propagation. Its contribution is in:
The abstraction is descriptive, not a claim of novelty.