Implementation Status

Three states

Specified. The field is defined in the spec with operational requirements and failure modes.

Formally Verified. The field is part of the machine-verified SymPy and Lean 4 conjunction.

In Record Schema. The field is a structured field in the JSON record schema that every governed record must populate.

A field can be specified and verified without yet being a schema field; the table below says which is which.

What "narrative field" means

"Narrative field" means the field 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, but not yet machine-parseable as a structured object; Schema v1.4 will formalise these as typed fields.

What "Not yet" means

PCF, P10, P11, P12 are specified and formally verified but are not yet present in governed records. The v1.4.3 structural integrity constraints (P2_DAG, P6_AtomicAgency, P1_Freshness, P4T_EnvInvariant) are formalised in the Lean bundle as of 25 April 2026. All of the above are specified in /omega/spec/v1/ and verified in /omega/formal-proof/. They are not yet produced in governed records.

We are publishing this honestly. Specification and verification precede implementation. Every field 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.3 Structural Integrity Constraints: Implementation Status

v1.4.3 adds structural integrity constraints (P1 freshness, P2 DAG enforcement, P6 atomic agency, P4T environment invariant, P_ChainIntegrity), formalised in the Lean bundle as P2_DAG, P6_AtomicAgency, P1_Freshness, P4T_EnvInvariant, and P_ChainIntegrity. These constraints are formally verified in the Lean 4 bundle (OmegaV14.lean) but are currently expressed as validation requirements on records rather than as enforced structured schema fields.

What this means in practice:

• Formally specified: Each constraint has a canonical prose definition, pattern, and technical mechanism (see specification §v1.4.3 Structural Integrity Constraints).
• Formally verified: The bundle is kernel-verified in Lean 4 via SafeVerify (2026-06-24; see formal proof).
• Validated at record level: Records declared as v1.4.3-conformant must satisfy the constraints at the time of governance review.
• Not yet enforced as schema: The constraints do not currently appear as independent structured fields in the OMEGA record schema. Schema enforcement is pending a subsequent release.

This distinction is important for integrators: claims of v1.4.3 conformance must be demonstrable against the prose constraints; the record schema does not independently verify the structural integrity properties.

Roadmap

Structured schema encodings for the Extended fields are not yet published; they publish when integrator demand or standards alignment (ERC-8004, UCAN) determines their encoding. Planned encodings:

• Structured JSON fields for P4M, P4T, P5E, P6, P6A, P6L (currently narrative)
• Schema enforcement of v1.4.3 structural integrity constraints: freshness window fields, DAG validation proofs, delegation chain expansion, environment assumption bindings, lift from record-level validation requirements to first-class schema fields.
• New top-level object primitive_continuity for PCF
• New top-level object primitive_competence for P10
• Extension of primitive_expectation with update_history for P11
• Extension of primitive_expectation with semantic_schema binding for P12

Why publish this

Specified, verified, and implemented are three separate claims. Protocols that blur the distinction between them lose credibility when any one is challenged.