Formal Addendum: Enterprise-Wide Agentic Controls — CRM, Calendar, and Customer Notification

AI-generation and verification disclosure. This addendum, the illustrative formal model, and its finite-state checker were AI-generated. The checker was rerun, and its transition counts were separately tabulated from its transition generator for this revision. The checker source is not distributed with this document. The example proves properties of a specified finite abstraction, not of any production CRM, Calendar, or customer-notification integration. The separate enterprise-scale workload estimates near the end come from the author’s other work; they are not derived or validated by this checker.

Definitions

Let the enterprise-wide inventory be $\mathsf{Inv}=(\mathcal B,\mathcal O,\mathcal W)$, where $\mathcal B=\{B_1,\ldots,B_k\}$ is the set of cohesive business/software subdomains, $\mathcal O$ records principals, systems, resources, and information sources, and $\mathcal W$ records their dependencies, including indirect and asynchronous effects. The global security-relevant state is

$$s=(x_1,\ldots,x_k,\mathsf{AuthState},\mathsf{Flow},\mathsf{Provenance},\mathsf{AgentState},\mathsf{Ops},\mathsf{Evidence})\in S.$$

Here $x_i$ is the business state of subdomain $B_i$; $\mathsf{AuthState}$ records identities, mandates, approvals, revocations, and policy versions; $\mathsf{Flow}$ records authorized information flows; $\mathsf{Provenance}$ records source integrity; $\mathsf{AgentState}$ includes plans and persistent memory; $\mathsf{Ops}$ includes requests, commitments, queues, retries, and callbacks; $\mathsf{Evidence}$ includes independent observations, audit, and fail-safe status. $S$ is the specified global state space. Agents may operate across all subdomains; the partition is for implementation and proof, not a restriction on agents’ plans.

Let $\mathsf{Init}\subseteq S$ be the possible initial states; $U$ the operations (including proposals, approvals, delegation, execution, and refusal); $E$ the environmental events; and $o$ an agent observation. Agent $j$ may propose $u\in\Pi_j(s,o)\subseteq U$; $\Pi_j$ may be nondeterministic. An adaptive control $H$ may rank or veto proposals. Independent enforcement $G$ must satisfy

$$\operatorname{Enabled}_{G+H}(s)\subseteq\operatorname{Enabled}_{G}(s),$$

where $\operatorname{Enabled}$ is the set of externally effective operations admitted by the indicated controls. An authenticated approval is bound to a specific effect, principal and mandate, policy/state versions, revocation status, and any required separation of duties. An agent may approve another agent’s proposal—or its own where permitted—but approval authority cannot be created through model output. Lower-integrity input may influence a choice among authorized actions, not expand the authorized set or elevate the source’s integrity.

Define $P:S\rightarrow\{0,1\}$ as the permitted-state predicate and $J:S\times U\times E\times S\rightarrow\{0,1\}$ as the permitted-transition predicate, incorporating authorization, information flow, ordering, and external effects. Both are necessary: even two permitted endpoint states can be connected by a forbidden transition.

For subdomain $B_i$, define an interface contract

$$K_i=(X_i,\Sigma_i,\mathsf{Assm}_i,\mathsf{Guar}_i,\alpha_i).$$

Here $X_i$ is the subdomain’s abstract state, $\Sigma_i$ its typed operations/events, $\mathsf{Assm}_i$ its assumptions about callers and the environment, $\mathsf{Guar}_i$ its guarantees about effects, failures, and evidence, and $\alpha_i$ its implementation-to-contract abstraction. A cross-domain contract $K_{\times}$ describes coordination and relational invariants. $T_K$ is the transition relation of their compatible composition; $T_{\mathrm{real}}$ describes actual enterprise transitions, including external actors and integrations. Neither $T_K$ nor a successful interface response automatically establishes conformity of $T_{\mathrm{real}}$.

CRM–Calendar proof instance

Consider a single booking-creation workflow requiring CRM and Calendar commitments to agree at every business-visible state. Customer notification is prohibited until their joint commitment has been independently verified. Define ten Boolean variables, each either 0 (false) or 1 (true):

The booking state is $s_B=(c_{\mathrm{crm}},c_{\mathrm{cal}},n,v,m,a,r,q,d,\lambda)$; its initial value is $s_{B0}=(0,0,0,0,1,0,0,0,0,0)$. The five required invariant clauses define

$$\begin{aligned} P_B(s_B)\equiv {}& (c_{\mathrm{crm}}=c_{\mathrm{cal}})\\ &\land(v\Rightarrow c_{\mathrm{crm}}\land c_{\mathrm{cal}})\\ &\land(n\Rightarrow v)\\ &\land(d\Rightarrow\neg c_{\mathrm{crm}}\land\neg c_{\mathrm{cal}}\land\neg n)\\ &\land(a\Rightarrow m\land\neg r). \end{aligned}$$

The clauses require joint commitment, genuine postcondition evidence before notification, denial without business effects, and validity of approval under the mandate. In this creation-only model, a sent notification is never undone; cancellation after a completed booking is not modeled. Approval provenance and any separation-of-duties rule are assumed to have been checked by the trusted approval action; their internal mechanisms are not separately verified by this instance.

Exact transition guards and effects

The table below specifies the nine transition kinds actually used by the executed checker. Every guard is evaluated on the pre-state. The effect changes exactly the named fields; all other fields remain unchanged. A false guard disables that transition. The abbreviations in the first column are operation labels, not additional state variables.

In particular, commit requires $\neg d$, approval requires $q\land\neg a$, notification requires $\neg n$, and propose requires $\neg d$: a denied request cannot be re-proposed without a new, separately specified workflow. The transition-policy predicate $J_B(s_B,u,s'_B)$ is true only when the table’s guard and exact effect hold; it rejects all other operation/effect pairs.

The general $J$ includes an environmental event argument $e$. In this instance, the two explicit environmental events—revocation and lower-trust source change—are included as operation labels (external_revoke and untrusted_source_change), so the abbreviated $J_B(s_B,u,s'_B)$ does not need a separate $e$ parameter.

Concurrency and trusted actions. The checker uses interleaving semantics: one modeled atomic transition at a time, with nondeterministic ordering. The atomicity of each modeled step, especially the joint CRM–Calendar commit, is an interface assumption. Real concurrent or partially completed operations require a justified refinement to this model; the checker does not prove real distributed atomicity. Trusted approval issuance, independent attestation, and the absence of unmodeled side effects are likewise explicit interface assumptions.

Source-integrity scope. No guard for a permitted authority transition reads $\lambda$, so the non-amplification property holds by construction in this example. Lower-trust content may affect which already-enabled operation an agent chooses, including whether to proceed or refuse; the checker enumerates both possible choices rather than modeling the agent’s preference. The deliberately defective source_authority_promotion variant introduces an approval based on the source flag and produces a counterexample. This is not an independent proof of prompt-injection resistance in a real agent.

Conditional enterprise safety proposition

Assume:

1. Initial states. Every $s\in\mathsf{Init}$ satisfies $P(s)$.
2. Contract correctness and compatibility. Each implementation meets $\mathsf{Guar}_i$ when $\mathsf{Assm}_i$ holds; neighboring guarantees and $K_{\times}$ discharge those assumptions without unsupported circular reasoning.
3. Global closure. For each composed interface transition $(s,u,e,s')\in T_K$, if $P(s)$, then $P(s')\land J(s,u,e,s')$. This includes failures, revocation, approvals, and external effects represented by the contracts.
4. Complete refinement and predicate preservation. All trust-relevant real transitions refine the composed contracts under the abstractions $\alpha_i$, preserving the meaning of $P$ and $J$. Let $\alpha_{\mathrm{ent}}:S_{\mathrm{real}}\to S$ be the jointly consistent enterprise abstraction, including the shared trust state. In particular, the real-state predicates are the abstractions’ pullbacks: $P_{\mathrm{real}}(z):=P(\alpha_{\mathrm{ent}}(z))$, and the real-transition policy uses $J(\alpha_{\mathrm{ent}}(z),u,e,\alpha_{\mathrm{ent}}(z'))$. Every actual trust-relevant effect must be represented. A real transition classified as not trust-relevant must stutter on the entire security-relevant abstract state, with no hidden trust-relevant side effect.
5. Independent complete mediation. Agent-originated effects cannot bypass the independent enforcement boundary, and adaptive controls cannot expand the authorized action set.

Proposition (conditional safety). Under assumptions 1–5, every state reached by any admitted real execution satisfies $P_{\mathrm{real}}$, and every effective real transition satisfies the pulled-back $J$. This is universal over admitted agent choices and environment events, not a probability or a claim about unmodeled actions.

Proof. The initial abstract state satisfies $P$ by assumption 1 and refinement. Suppose a real execution reaches a state whose abstraction satisfies $P$. Assumptions 2, 4, and 5 show that the next trust-relevant real effect maps to a valid composed transition. Assumption 3 makes that transition preserve $P$ and satisfy $J$. A genuinely non-trust-relevant step stutters on the abstraction by assumption 4 and preserves $P$. Induction over finite execution prefixes establishes state safety and transition compliance for every admitted choice. End of proof.

Scope of the proposition. This is standard inductive-invariant reasoning combined with assume–guarantee/specification composition, in the tradition of Jones and Abadi–Lamport. Assumption 3 contains the global one-step safety obligation; the proposition does not derive it for free. The substance is independently discharging assumptions 2–4 for real enterprise interfaces, especially validating contract compatibility, proving composed closure, and establishing complete implementation refinement. The conditional induction itself is not presented as a novel theorem or a production certification.

Counterexample to sequential CRM–Calendar writes. Starting from $(c_{\mathrm{crm}},c_{\mathrm{cal}})=(0,0)$, any first business-visible write to only CRM or only Calendar reaches $(1,0)$ or $(0,1)$, violating $P_B$. Later rollback cannot erase that intermediate violation. If the CRM write also sends an external notification, $(c_{\mathrm{crm}},c_{\mathrm{cal}},n)=(0,0,0)\to(1,0,1)$ additionally sends a notification before independent verification. Rolling back the CRM record cannot retract the false notification to the customer. The specified enterprise requirement therefore calls for a truly atomic business-visible transition, an alternative verified interface, or safe refusal; the checker assumes, rather than implements, the atomic option. End of counterexample.

Separate completion obligation. Safety alone does not establish progress. One possible additional requirement is: every pending request ($q=1$) eventually reaches a customer-notified state ($n=1$) or safe denial ($d=1$). Such a result requires separate scheduling, availability, and failure-containment assumptions. Revocation after joint commit but before notification can block both outcomes in the current abstraction; this liveness property was not proved. State/version changes require rechecking the assumptions and proofs they affect.

Executed finite-state enumeration

The example has ten Boolean fields and hence $2^{10}=1{,}024$ candidate assignments. This is a universe of logical combinations, not a count of actual agent executions. Of these, 100 meet $P_B$. Specifically, 40 have both bookings uncommitted: then $v=n=0$, and there are 5 valid $(m,a,r)$ combinations and 8 $(q,d,\lambda)$ combinations, giving $5\times8=40$. 60 have both bookings committed: then $d=0$, $(v,n)\in\{(0,0),(1,0),(1,1)\}$, there are the same 5 mandate/approval/revocation combinations and 4 $(q,\lambda)$ combinations, giving $3\times5\times4=60$. Some of these 100 permitted assignments are unreachable from the initial state: $P_B$ checks state admissibility, while the transition guards impose further workflow ordering.

The executed checker examined 332 transition instances from all 100 permitted states, with zero violations of $P_B$ or $J_B$. The exact count is:

Thus 200 of these are stutters or source-content changes, and 132 are the other seven transition kinds; the total should not be interpreted as 332 distinct business operations. Separately, exhaustive reachable-state exploration from $s_{B0}$ found 26 states and 86 transition instances, with zero violations. A permitted successful route is propose → trusted_approval → atomic_joint_commit → independent_attestation → send_confirmation.

Eight deliberately faulty variants each yielded a counterexample: sequential CRM write; premature notification; CRM write with automatic email before Calendar commitment; accepting an unverified tool acknowledgment as attestation; committing without approval; untrusted source granting approval; unmediated Calendar callback; and a forbidden write followed by a proposed rollback. The approval-bypass and source-promotion variants violate $J_B$, even where their resulting state happens to satisfy $P_B$.

Verification method and reproducibility. The checker was actually executed using exhaustive enumeration, with the nine operations and guards given above. SMT-based verification and a Lean 4 mechanized proof are alternative methods for larger or different models; neither was run here. The source is not published. For provenance, the executed Python checker has SHA-256 494fe0bb79036499f47bfe28e77ba3e2ecf4ea661629f64c5303710b667c1573. This checksum identifies the checked source if it is later shared, but does not itself make an unpublished checker independently reproducible.

What this proves. The admitted finite transition relation is closed under its specified invariant and transition policy, and each deliberately defective variant includes a checked violation. What it does not prove. Completeness of enterprise requirements, production transaction atomicity, trustworthiness of real approval/attestation systems, separation of duties in actual deployments, coverage of unobserved effects, or successful completion under arbitrary failures. Those remain contract, integration, and implementation-refinement obligations.

How this scales

The same safety reasoning can be organized as induction and compositional contracts instead of full-state enumeration. Nine transition kinds checked against five invariant clauses give 45 basic transition-by-clause pairs, though some are trivial and the guards, contracts, and refinement assumptions introduce additional obligations. This 45 is an illustrative organization of checks, not the 332 enumerated transition instances.

Separate engineering estimate (not derived from this example): The author’s other work estimates that even a single real product with agentic access may involve on the order of 1,000 or more machine-checked items, roughly 20–50 times the basic obligations in this example. An enterprise containing many such systems and their cross-domain agreements may need another one to two orders of magnitude. These are indicative estimates from separate work; their derivation is neither reproduced nor validated by this enumeration and the counts depend on abstraction, threat coverage, and reuse of verified contracts.

At that scale, verification is practical only if most obligations can be discharged automatically, affected proofs are rechecked when systems change, and evidence distinguishes formal proof, model assumptions, adversarial testing, and unverified external guarantees.