An agent’s proposed action and the system’s permission to execute it are different things. The Certified Execution Harness paper formalizes the layer between an LLM and its tools using Petri nets, studying how execution controls behave under prompt injection and repeated replanning.
Represent permission as an execution condition
In the model, marks represent capabilities, approvals and budgets. A transition can fire only when its required marks are present. An injected request with unmet or spent preconditions is therefore refused regardless of how it is worded.
The paper treats tool outcomes as uncontrollable and applies a conventional maximally permissive supervisor. Its safety result transfers to a running system under four assumptions. Those conditions are part of the claim: the formal result should not be read as unconditional protection for every agent framework or tool integration.
Refusal can change the next proposal
The researchers add a replanning closed loop in which an agent can propose another action after a refusal, spending an inference call each time. They show that the conventional supervisor can be arbitrarily more intrusive than a stricter safe supervisor in this loop.
This makes the problem more subtle than allowing every action that appears safe in isolation. A controller’s choices can affect retries, cost and the agent’s subsequent path. The paper characterizes a least-intrusive supervisor for a given proposer model through a value-threshold refinement.
Examine the whole workflow
In an autonomous release-agent example, the authors find by synthesis that safe deployment requires a step that a supervisor can refuse after rollout begins. That result highlights the need to reason about the workflow, including what remains possible after an earlier action has executed.
A practical evaluation should map each formal precondition to an actual enforcement point and test the assumptions around tool outcomes and retries. Record refused proposals as well as executed actions. This is a formal research treatment of execution control, not a ready-made guarantee that a particular production release process is safe.
Comments