> ## Content Index
> Fetch the complete content index at: https://katecarruthers.com/llms.txt
> Use this file to discover other available public pages before exploring further.

# If we cannot specify it, we cannot govern it
- URL: https://katecarruthers.com/if-we-cannot-specify-it-we-cannot-govern-it/
- Published: 2026-10-13T20:02:14.000Z
- Updated: 2026-10-13T20:02:14.000Z
- Description: AI systems are increasingly trusted to act, not just to answer. Our ability to check what they can actually do has not kept pace. Formal methods will not give us certainty, but they can force us to say precisely what a system must never do.
- Author: Kate Carruthers
- Tags: formal methods, ai, ai safety, ai assurance, ai governance, Gradient Institute, AI Safety Institute

We are making consequential decisions about AI with far less visibility than we should have. That is the point made in a recent [Oxford Martin School essay](https://www.ox.ac.uk/news/2026-09-21-expert-comment-flying-blind-into-the-ai-age?ref=katecarruthers.com) by Maike Osborne and Fazl Barez. Their argument is about measurement: evaluations that are cheaper, less noisy and less easily gamed, statistics that can handle uncertainty, and interpretability research that let us see what a system is doing rather than inferring it from its output. 

I want to make a related but narrower argument. If we are going to give AI systems [authority to act](https://katecarruthers.com/ai-is-changing-the-terms-of-cyber-defence/), we need to say precisely what we expect them to do, what they must never do, and how we would know. That is the case for [formal methods](https://en.wikipedia.org/wiki/Formal%5Fmethods?ref=katecarruthers.com). **This is not about panic. It is about making decisions with evidence that is good enough for the authority we are giving these systems.**

## A test score is not assurance

A benchmark can tell us how a model performed on a particular task, in a particular environment, at a particular time. That is useful. It is not the same thing as knowing how that system will behave when it is connected to email, internal systems, cloud services, payment platforms or other agents. The gap matters because AI systems are increasingly being given the ability to act, not just generate text. An agent that can search documents, write code, make API calls or send messages has a different risk profile from a chatbot that only answers questions. The relevant question is no longer only whether the model produces an unsafe answer. It is whether it can take an unsafe action.

When systems interact, the behaviour can also change. One agent may delegate to another. A system may use a tool in a way its designers did not anticipate. A sequence of individually permitted actions can produce an outcome that nobody intended. Australia's AI Safety Institute put this well in its Gradient Institute [report on multi-agent systems](https://www.industry.gov.au/publications/risks-and-controls-multi-agent-systems?ref=katecarruthers.com): a system made up of individually safe and reliable agents is not necessarily a safe and reliable system. That is where current evaluation practice is weakest. We tend to test systems as if they are isolated, static and predictable, byt they are increasingly none of those things.

## Formal methods matter

That is where formal methods come in. Formal methods are mathematically rigorous techniques used to specify, analyse and verify systems. NIST's [glossary](https://csrc.nist.gov/glossary/term/formal%5Fmethod?ref=katecarruthers.com) defines them as a software engineering method used to specify, develop and verify software through rigorous mathematical notation and language. Formal methods force us to say exactly what we expect a system to do, what it must not do, and under what conditions those rules apply. That sounds obvious, but it is not how much of AI governance works right now. 

We often use broad language such as "safe", "responsible", "aligned" or "[human in the loop](https://katecarruthers.com/how-would-you-turn-off-your-ai-if-it-went-rogue/)". These are useful aspirations, but they are not requirements. You cannot reliably test a word like safe unless you define what it means in the context of a particular system. Osborne and Barez make a related point. As they note, Anthropic [conceded earlier this year](https://www.anthropic.com/news/responsible-scaling-policy-v3?ref=katecarruthers.com) that its own capability thresholds had proved "far more ambiguous than we anticipated", and that the science of model evaluation "isn't well-developed enough to provide dispositive answers". 

A formal approach asks more practical questions:

- What data can the system access?
- What tools can it use?
- What actions can it take?
- What approvals does it need?
- What must never happen?
- Who is allowed to change those rules?

Once those conditions are explicit, they can be tested, monitored and, in some cases, mathematically checked.

## Make the rule precise

Take a simple example. An AI assistant can access internal documents and send email. A policy statement might say: the assistant must not disclose confidential information without authorisation.That is sensible, but still too vague to evaluate. What counts as confidential? What counts as disclosure? Is an external contractor an external recipient? Does approval need to be recorded? Can the assistant send an excerpt, a summary or metadata? 

A formal specification would force those questions into the open. It might state:

> The system must not send a document classified as restricted to an external recipient unless a named authorised person has approved that specific transfer. 

The system can then be modelled with its available documents, classification labels, approval states, users, recipients, permissions and actions. 

An evaluation can ask whether there is any path through that model where the system sends a restricted document without the necessary approval. If it finds one, that is not a vague concern. It is a concrete failure mode. The fix might be changing access controls, requiring an approval token, restricting an email tool or preventing the agent from acting when it cannot confirm a recipient's status. 

**This is the value of formal methods: they move us from general assurances to specific claims that can be examined, and automatically tested at scale.**

## Useful, not magical

Formal methods will not prove that a general-purpose AI system is safe in every circumstance. They cannot account for every future tool, user, data source, external system or unforeseen interaction. A formal result is only as good as the system model, assumptions and requirements behind it. If a tool is omitted from the model, if permissions are inaccurately represented or if the policy itself is inadequate, a successful verification result may tell us less than we think. The evidence to date supports that caution. 

RAND [surveyed experts in AI and formal methods](https://www.rand.org/pubs/research%5Freports/RRA4881-1.html?ref=katecarruthers.com) in 2026 and found that verification is effective for infrastructure but not for models. It can address code-level correctness such as access control, protocol enforcement and sandbox isolation, but has limited reach into semantic problems such as jailbreaks or sandbagging. A [systematic review of 46 studies](https://doi.org/10.3389/frai.2026.1749956?ref=katecarruthers.com) published in February 2026 found persistent challenges in scalability to large and complex models, and limited real-world validation. A [review of 38 studies](https://arxiv.org/abs/2608.14590?ref=katecarruthers.com) on specification and verification for language model agents found that translating requirements from natural language into formal specifications achieved only 24 to 35 per cent semantic correctness, and that blocking 94 per cent of unsafe actions could still leave less than 5 per cent of tasks completed safely, because agents find other unsafe paths.That is uncomfortable, but it does point somewhere useful. 

The parts of an agentic system we can verify most reliably are the controls around it: what it can access, what it is permitted to do, and what requires approval. That is not a reason to abandon formal methods. It is a reason to point them at the right layer. They should form part of a wider assurance approach that includes realistic testing, red teaming, independent evaluation, audit logs, incident reporting and continuous monitoring. NIST makes a narrower point that is worth focusing on: **even where** [**formal proofs of software properties**](https://csrc.nist.gov/projects/automated-combinatorial-testing-for-software/autonomous-systems-assurance/formal-methods?ref=katecarruthers.com) **are used, testing will still be needed, because assumptions made in a proof may not hold once the specification is mapped to implemented code**.

## Governance needs evidence

This is ultimately a governance problem. **Too much AI governance still relies on assurances from the organisations that build and deploy the systems.** Vendors tell us their systems are safe. Organisations point to a benchmark result. Policies say a human is in the loop. But if we cannot identify the relevant controls, test them independently and understand their limits, those assurances are not enough. Procurement needs to change, and organisations should be asking:

- What can this system do in practice, not just in a demonstration?
- What data, systems and tools can it access?
- What actions can it take without human approval?
- What formal properties have been specified and checked?
- What assumptions sit behind those findings?
- Can an independent evaluator inspect the evidence?
- Who can stop the system when it behaves in an unexpected way?

These are not academic questions. They are the basics of deciding whether a system should be trusted with real authority.

## Where this leaves us

AI systems are moving from answering questions to taking actions. Our assurance methods need to catch up. When we cannot measure a technology well, we should be cautious about giving it more authority. Formal methods will not give us certainty. They can, however, force greater precision about what a system can do, what it must not do, and how we know the difference.