FORMAL METHODS

Prove the boundary, not the intelligence.

NO_UNGOVERNED_CAUSAL_EFFECT_PATH is an absence-of-bad-paths safety property. The model may treat the AI or worker as an adversarial black box. The formal obligation sits in the mediation architecture around it.

The property

No path U → C may succeed without crossing B. U = untrusted computation/state C = relevant external consequence B = governed effect boundary ExternalEffect(e) ⇒ KnownBoundary(e) ∧ ExactEffectBound(e) ∧ AuthorizedNow(e) ∧ DenyEnforceable(e) ∧ FailClosed(e) ∧ Evidenced(e)

Methods

Information-flow / non-interference

Model untrusted-to-external influence as prohibited flow except through controlled release points corresponding to governed boundaries.

Capability and effect systems

Remove ambient authority so external effects are impossible without an explicit capability presented at a governed boundary.

Model checking

Check reachability over causal/dependence graphs or state machines. TLA+/TLC is the reference bounded model for current VALO work.

Theorem proving

Use TLAPS, Lean, Coq, Isabelle/HOL or equivalent for deductive proof of the abstract mediation property.

Static / abstract analysis

Over-approximate data, control and effect flows; if no ungoverned path exists even in the over-approximation, that is strong code-level evidence.

Runtime verification

Continuously check path inventory, provenance, capability use and enforcement because production topology can drift after static proof.

TLA+ reference model

The Kernel formalization models the untrusted component as able to attempt every declared channel. Ungoverned attempts are allowed as attempts but must produce NULL external effect. Successful external effects record a known boundary plus authorization, enforcement and evidence.

AttemptUngovernedEffect(c) → blockedAttempts + 1 → externalEffects unchanged GovernedEffect(c,b) → known boundary → authorized now → enforced → evidenced → externalEffects + 1

The bounded TLC model is formal evidence over the declared abstraction. It is not evidence that a real deployment has inventoried every path.

Deployment proof remains separate

A formal architecture proof and a deployment conformance claim are different artifacts. Production must still inventory actual reachable paths, map them to enforcement, fail closed on unknowns, preserve evidence and re-verify after topology/configuration/plugin/credential/operator changes.

Architecture asks: can the design permit an ungoverned path?
Deployment asks: does this concrete installation contain one?

Current implementation status

The Kernel implementation branch contains executable causal-capacity contracts, negative tests and the TLA+ model. REHT Standard v0.7 adds boundary-quality and additional-channel conformance cases. These new formalization additions require the normal local-only validation process before a new receipt is marked COMPLETE.

No GitHub Actions or remote CI is part of that validation path.