We believe the relationships between a specification, its implementations, and the agents allowed to change or execute them need to be formalized explicitly. These questions are crucial, but we do not yet see a sufficiently established treatment that brings them together for the systems we are building. This paper proposes a shared foundation, with clear distinctions between preserving meaning, making progress, recovering an observable state, and staying within granted authority.

Asking agents to organize all of this for themselves, and trusting them to leave behind a comprehensible formalization, is not a route to scale that we are willing to rely on. We expect repeated invention of the same foundations, incompatible structures, and a growing review burden. At worst, the workflows and formal reasoning become impossible for human reviewers and auditors to follow, even when individual proofs check. A shared framework should make those choices explicit and keep them open to inspection.

The Cubical Agda formalization is work in progress. We expect a first formalized version before the end of November 2026. Writing proof-assistant code is not the bottleneck: human review, and reaching agreement on the specification to lock for that first version, take the time.

We already use different variants of this framework across our solutions. That experience is helping us understand how decisions in the low-level foundations affect robustness in production. We are using those lessons to refine the common framework as the formalization develops.