Trust Algebra

The Problem #

Classical proof assistants like Lean, Coq, and F* operate with a single, binary trust bit: a term either type-checks or it does not. This is perfectly appropriate for a closed, fully-interactive proof session, but it is severely limiting in the environment where JuGeo operates — a heterogeneous, live Python codebase with evidence arriving from many sources simultaneously.

Without a unified gradation, a system is forced to either reject all non-proof evidence (too strict for everyday development) or silently promote weak evidence to proof status (dangerous). JuGeo solves this with the Trust Ordered Algebra \(\mathfrak{T}\).

The Trust Ordered Algebra #

Formally, the Trust Ordered Algebra is the six-tuple

where the components are:

• \(\mathcal{E}_{\text{adm}}\) — the carrier set of admissible evidence items: everything JuGeo can attach a trust level to (Z3 certificates, test logs, Lean terms, LLM proposals, …).
• \(\preceq\) — the partial order on trust levels, with \(\texttt{CONTRADICTED} \preceq \texttt{UNVERIFIED} \preceq \cdots \preceq \texttt{VERIFIED\_PROOF}\).
• \(\oplus\) — the conservative join (composition): combines two evidence items by taking the weaker of their trust levels.
• \(\ominus\) — attenuation: models trust weakening that occurs when evidence is transported across sheaf restriction maps.
• \(\uparrow_{\!\pi}\) — promotion: explicit strengthening of a trust level along a named policy route \(\pi\), always logged to the audit trail.
• \(\downarrow_{\!\chi}\) — demotion: ceiling enforcement in response to a challenge \(\chi\); trust may only fall, never silently rise.

Trust Levels #

\(\mathcal{E}_{\text{adm}}\) is stratified into seven named levels forming a total preorder embedded in \(\preceq\). Each level corresponds to a concrete kind of evidence that JuGeo can produce or consume.

The Partial Order #

Levels are totally ordered under \(\preceq\):

Formally, the order is given by the integer ranking above: \(t_1 \preceq t_2 \iff \text{rank}(t_1) \le \text{rank}(t_2)\). This makes \(\mathcal{E}_{\text{adm}}\) a seven-element chain under \(\preceq\).

Operations #

Four operations act on trust levels (and on full evidence profiles carrying those levels). Together they define the algebraic structure of \(\mathfrak{T}\).

The Three Laws #

Three invariants are enforced system-wide. Violations raise JuGeoError at runtime and are flagged as verification failures in the audit log.

Python Examples #

Creating and Inspecting Trust Profiles

A TrustProfile records the trust tier, the evidence scope, and the chain of reasons that produced it.

from jugeo.evidence.trust import TrustLevel, TrustProfile, TrustTier

# Create a profile at COPILOT_SUGGESTED level
profile = TrustProfile(
    tier=TrustTier.COPILOT_SUGGESTED,
    scope=("spec.affine.program.00",),
    reasons=("copilot-proposal",),
)

print(profile.tier)       # TrustTier.COPILOT_SUGGESTED
print(profile.rank)       # 2
print(profile.is_at_least(TrustTier.RUNTIME_WITNESSED))  # False
print(profile.is_at_least(TrustTier.UNVERIFIED))         # True

Silent Promotion is Rejected

Calling promote() without an explicit policy route and audit reason raises JuGeoError immediately, enforcing Law I.

from jugeo.evidence.trust import TrustProfile, TrustTier
from jugeo.errors import JuGeoError

profile = TrustProfile(
    tier=TrustTier.COPILOT_SUGGESTED,
    scope=("spec.affine.program.00",),
    reasons=("copilot-proposal",),
)

# Silent promotion → raises JuGeoError  (Law I violation)
try:
    profile.promote(TrustTier.VERIFIED_PROOF)
except JuGeoError as e:
    print(e)
# JuGeoError: silent promotion from COPILOT_SUGGESTED to VERIFIED_PROOF
# is not permitted. Provide explicit=True and a named reason.

Explicit, Audited Promotion

With explicit=True and a named reason, promotion is permitted and an audit entry is written automatically.

from jugeo.evidence.trust import TrustProfile, TrustTier

profile = TrustProfile(
    tier=TrustTier.COPILOT_SUGGESTED,
    scope=("spec.affine.program.00",),
    reasons=("copilot-proposal",),
)

# After Z3 confirms the arithmetic goal:
promoted = profile.promote(
    TrustTier.SOLVER_DISCHARGED,
    explicit=True,
    reason="z3-confirmed-arithmetic",
    policy_route="smt-dispatch-v2",   # named policy route π
)

print(promoted.tier)     # TrustTier.SOLVER_DISCHARGED
print(promoted.reasons)
# ("copilot-proposal", "z3-confirmed-arithmetic")

# Audit trail is automatically persisted
for entry in promoted.audit_log():
    print(entry)
# AuditEntry(op='promote', from_tier=COPILOT_SUGGESTED,
#            to_tier=SOLVER_DISCHARGED, policy='smt-dispatch-v2',
#            reason='z3-confirmed-arithmetic', ts=2026-03-23T...)

Composing Evidence Items

The compose() method applies the conservative join (\(\oplus\)), returning a new profile whose tier is the minimum of the two inputs.

from jugeo.evidence.trust import TrustProfile, TrustTier

solver_ev = TrustProfile(
    tier=TrustTier.SOLVER_DISCHARGED,
    scope=("spec.arithmetic",),
    reasons=("z3-unsat",),
)

copilot_ev = TrustProfile(
    tier=TrustTier.COPILOT_SUGGESTED,
    scope=("spec.arithmetic",),
    reasons=("gpt4-proposal",),
)

# Conservative join: SOLVER_DISCHARGED ⊕ COPILOT_SUGGESTED = COPILOT_SUGGESTED
composite = solver_ev.compose(copilot_ev)
print(composite.tier)  # TrustTier.COPILOT_SUGGESTED   (Law II)

# Composed reasons are unioned
print(composite.reasons)  # ("z3-unsat", "gpt4-proposal")

Handling Challenges

When a challenge arrives (e.g., a monitoring assertion fires at runtime), the challenge() method applies \(\downarrow_\chi\) and may lower the trust level to CONTRADICTED.

from jugeo.evidence.trust import TrustProfile, TrustTier, Challenge

# A profile that previously held SOLVER_DISCHARGED
profile = TrustProfile(
    tier=TrustTier.SOLVER_DISCHARGED,
    scope=("spec.bounds",),
    reasons=("z3-bounds-check",),
)

# A counterexample was found at runtime
cx = Challenge(
    kind="runtime-counterexample",
    payload={"input": -1, "output": "IndexError"},
    ceiling=TrustTier.CONTRADICTED,
)

demoted = profile.challenge(cx)
print(demoted.tier)    # TrustTier.CONTRADICTED  (Law III)
print(demoted.reasons)
# ("z3-bounds-check", "challenged:runtime-counterexample")

Trust in Evidence Bundles #

In practice, JuGeo's multi-channel evidence system assembles Evidence Bundles — structured collections of evidence items from heterogeneous sources (static analysis, Z3, runtime monitoring, copilot, Lean). Each item carries its own TrustProfile, and the bundle computes a combined trust for downstream consumers.

The conservative join across all channels means the bundle's trust is bounded by its weakest contributor. To raise the bundle's trust, every channel contributing at a lower level must be either:

1. Replaced with a stronger evidence item for that channel, or
2. Dropped from the bundle scope (if the channel is not required), or
3. Explicitly promoted via a named policy route that covers the gap.

Trust Across Sheaf Restrictions

JuGeo models code as sections of a sheaf over a site of semantic scopes. When evidence is restricted from a broad scope (a whole module) to a narrow one (a single call-site), the trust level may attenuate:

This captures the intuition that a proof about a module does not necessarily transfer unchanged to a specific call-site with different preconditions. Attenuation is computed automatically by the restriction functor; developers do not need to manage it manually.

Summary #

The Trust Ordered Algebra gives JuGeo a principled, auditable way to handle the full spectrum of evidence that arises in real software verification — from an LLM's first suggestion to a fully mechanically checked Lean proof. The key properties are: