Certify, Then Act: Formal Safety Certificates for Cooperative LLM Agents in Stochastic Environments

Large language model (LLM) agents are increasingly asked to act, to move robots, edit live systems, and coordinate with other agents, rather than merely to answer questions. When deploying these systems in safety critical settings, average-case competence is not enough: a single low-probability unsafe action can be costly or irreversible. We propose a protocol whereby LLM agents can obtain and respect formal safety certificates in stochastic, cooperative, multi-agent environments. Specifically, we introduce the certify-then-act protocol in which independent LLM agents negotiate a joint contract, certify it using a sound probabilistic model checker that computes the probability of the contract leading to an unsafe state, and execute it only once that probability falls below a pre-specified threshold. This process is then repeated whenever random disturbances void the certificate. We instantiate the protocol in two stochastic cooperative domains, (a windy Gridworld and a collapsing Blocksworld), spanning six scenarios, and run a full factorial study over certification regime, communication, and base model. We find that (i) communication is highly beneficial; given communication it is enforcement rather than availability of the verifier that buys safety, with unsafe terminations falling from 17.3% to 0.0%; (ii) there is a trade off between guarantees of safety and task completion within a given budget; and (iii) models show a clean capability gradient. Certification comes with extra costs in additional actions and tokens, however, without these extra resources the enforced agents time out maintaining safety rather than fail unsafely. Additionally, we show heterogeneous pairs typically match or exceed their members' individual averages. We believe our results indicate equipping LLM agents with model checking tools presents an essential step toward deploying AI in safety critical Multi-Agent Systems.