Formal Model

Formal Model

The precise semantics of what a verdict means. The model is a non-normative appendix (spec/UST-1.0-formal-model.md); the spec and the Reference Checker are what conform to it. This page is the intuition, not the mathematics.

Verification is a measurability test

The three tiers are three nested σ-algebras — 𝒮_LIGHT ⊆ 𝒮_HIGH ⊆ 𝒮_TOP — over the space of possible worlds consistent with your information:

• A verdict names the finest tier decidable from your information set. With only the bytes and the key, you can decide LIGHT. Add the resolved name binding and you can decide HIGH. Add a verified anchor and you reach TOP.
• INDETERMINATE means the needed σ-algebra is not in your information set — the witness was unreachable, or an optional algorithm is unimplemented. It is cannot decide, structurally distinct from INVALID (decided: forged).
• Two conforming verifiers agree because the verdict is a total deterministic function of the §14a obligations table — same bytes and same world-coordinates ⇒ same verdict, on any machine, in any language.

Assurance is a product lattice

The assurance state is a tuple (integrity × identity × freshness × time) — a point in a product lattice, each axis a finite total order of earned strengths. The classic tier (LIGHT/HIGH/TOP) is one monotone policy projection of that lattice. Two consequences the checker enforces:

• No rung without its predicate. A strength coordinate is earned only from a verified seam verdict — a bare label, a caller boolean, or a look-alike object earns nothing.
• No upward forge, downgrade-resistant. You cannot mint a higher coordinate you didn't earn, and a missing input degrades the tier rather than failing the whole verdict.

Why a model at all

Trust infrastructure is worth only as much as the argument that it's sound. The model states the theorems; the conformance vectors witness each one (every theorem the model cites is a real check, kept in lockstep with the code). A witnessed check is not yet a proof — closing that gap in both directions is the Formal-model milestone:

• an independent human / expert review of the model itself, and
• a machine-checked proof (the L2 Lean milestone).

If you reason about UST beyond running the verifier, reason from here — not from analogy to JWT, JWS, or blockchain receipts.