Specified. Verified. Implemented. Three different things.
Specification reference: Current v1.4 (21 April 2026); prior specification (20 April 2026).
OMEGA v1.4 specifies fifteen primitives. All fifteen are formally verified in SymPy and Lean 4 as a minimal, consistent, independent decomposition (including the v1.4 structural integrity layer in the 21-conjunct Lean bundle; see formal proof). The production record schema (v1.0) implements five primitives as structured JSON fields. Ten primitives are either recorded as narrative fields in governed records or are pending schema extension.
This page shows exactly where each primitive sits today.
Three states every primitive can be in:
Specified. The primitive is defined in the spec with operational requirements, failure modes, and relationships to other primitives.
Formally Verified. The primitive is part of the machine-verified SymPy and Lean 4 conjunction. Verified as necessary, sufficient, independent, compensation-proof.
In Record Schema. The primitive is a structured field in the JSON record schema that every governed record must populate.
A primitive can be specified and verified without yet being a schema field. A primitive can be a schema field before it is verified. We say which is which, for every primitive, below.
| Primitive | Specified | Formally Verified | In Record Schema | Status |
|---|---|---|---|---|
| P1 Governance | v1.0 | v1.0 + v1.4 | v1.0 (primitive_governance) | Implemented |
| P2 Reasoning | v1.0 | v1.0 + v1.4 | v1.0 (primitive_reasoning) | Implemented |
| P3 Traceability | v1.0 | v1.0 + v1.4 | v1.0 (primitive_traceability) | Implemented |
| P4 Expectation | v1.0 | v1.0 + v1.4 | v1.0 (primitive_expectation) | Implemented |
| P5 Confirmation | v1.0 | v1.0 + v1.4 | v1.0 (primitive_confirmation) | Implemented |
| P4M Materiality Binding | v1.1 | v1.1 + v1.4 | Narrative field | Schema extension planned |
| P4T Trajectory Expectation | v1.2 | v1.2 + v1.4 | Narrative field | Schema extension planned |
| P5E Execution Attestation | v1.1 | v1.1 + v1.4 | Narrative field | Schema extension planned |
| P6 Delegation | v1.1 | v1.1 + v1.4 | Narrative field | Schema extension planned |
| P6A Aggregate Materiality | v1.2 | v1.2 + v1.4 | Narrative field | Schema extension planned |
| P6L Liability Threshold | v1.2 | v1.2 + v1.4 | Narrative field | Schema extension planned |
| PCF Continuity-Formal | v1.2 | v1.2 + v1.4 | Not yet | Specified and verified; schema pending |
| P10 Competence Attestation | v1.4 | v1.4 | Not yet | Specified and verified; schema pending |
| P11 Expectation Update Integrity | v1.4 | v1.4 | Not yet | Specified and verified; schema pending |
| P12 Semantic Integrity Validation | v1.4 | v1.4 | Not yet | Specified and verified; schema pending |
| P2_DAG | v1.4 | v1.4 | Not yet | Formalised in Lean bundle, 21 April 2026 |
| P6_AtomicAgency | v1.4 | v1.4 | Not yet | Formalised in Lean bundle, 21 April 2026 |
| P1_Freshness | v1.4 | v1.4 | Not yet | Formalised in Lean bundle, 21 April 2026 |
| P4T_EnvInvariant | v1.4 | v1.4 | Not yet | Formalised in Lean bundle, 21 April 2026 |
"Narrative field" means the primitive appears as a text field in the governed record but is not yet a structured JSON object with defined subfields. For example, P6L Liability Threshold currently appears as:
Liability threshold: P6L active, HIGH consequence confirmed
The field is present and auditable. It is not yet machine-parseable as a structured object with threshold values, escalation triggers, and cumulative risk counters. Schema v1.4 will formalise these as typed fields.
Four primitives, PCF, P10, P11, P12: are specified and formally verified but are not yet present in governed records. The four v1.4 structural integrity constraints (P2_DAG, P6_AtomicAgency, P1_Freshness, P4T_EnvInvariant) are formalised in the Lean bundle as of 21 April 2026. All of the above are specified in /omega/spec/v1/ and verified in /omega/formal-proof/. They are not yet produced by the Decision API or displayed in /omega/governed-systems/.
We are publishing this honestly rather than claiming otherwise. Specification and verification precede implementation. Every primitive in OMEGA followed this sequence: P4M was specified in v1.1 before it appeared as a narrative field; structured schema extensions follow once the operational definitions have stabilised under adversarial review.
v1.4 adds four structural integrity constraints (P1 freshness, P2 DAG enforcement, P6 atomic agency, P4T environment invariant), formalised in the Lean bundle as P2_DAG, P6_AtomicAgency, P1_Freshness, and P4T_EnvInvariant as of 21 April 2026. These constraints are formally verified in the 21-conjunct Lean 4 bundle but are currently expressed as validation requirements on records rather than as enforced structured schema fields.
What this means in practice:
This distinction is important for integrators: claims of v1.4 conformance must be demonstrable against the prose constraints; the record schema does not independently verify the four structural integrity properties.
Schema v1.4 is in development.
Schema v1.4 will formalise:
primitive_continuity for PCFprimitive_competence for P10primitive_expectation with update_history for P11primitive_expectation with semantic_schema binding for P12The v1.0 schema remains the canonical record format during the transition. Records produced under Schema v1.0 will remain conformant. Schema v1.4 is additive, not breaking.
Specified, verified, and implemented are three separate claims. Protocols that blur the distinction between them lose credibility when any one is challenged. OMEGA separates them.
Every audit has strengthened the standard. Naming what is not yet implemented is the same discipline as naming honest limits that cannot be closed: both are evidence that the standard is real rather than aspirational.