TL;DR. Agentic AI has inverted fifty years of coding: the language is the operative artefact now, and the regulators who can ask you about it assume you wrote it like an adult. The business rules community (SBVR, RuleSpeak) has been working on this since the 1970s and nobody listened. There are five things you have to control to write a sentence safe to put in front of an autonomous system. The tables at the end give you the lot.
And by the way, if all of this is too much for a Bank Holiday Monday morning, then I know a very willing llm who is just a cut and paste away from being able to draft better instructions….
Out of a clear blue sky….
Imagine, for a moment, that you are about to have a very bad afternoon.
Across the table sit two people from Compliance, one from Legal, and a man you have not previously met whose lanyard says External Counsel and whose expression suggests he charges by the minute and is in no hurry. On the screen between you is a transcript. The transcript is of an exchange between a customer and an autonomous agent which you, six months ago, configured. The agent has done something β you are not yet sure what, exactly, but you can tell from the seating arrangement that it was not good β and the question on the table, asked with the flat patience of someone who is going to ask it several more times before lunch, is: what, precisely, did you instruct it to do?
You open the document.
The document is called agent-prompt-v3-FINAL-actually-final.md. It is two thousand three hundred words long. It contains, by my rough count, four occurrences of the word “robust”, two of the word “thoughtful”, one parenthetical aside that begins “(obviously)”, and a bulleted list whose third item appears to contradict its first. It begins, “You are a helpful assistant.”
There is, at this point, very little anyone can do for you.
This essay is about how we got here, and what β if anything β half a century of work by a small, largely unfashionable group of people called the business rules community might have to say about it. Call it, if you like, a war on error: a long, unglamorous, mostly clerical campaign against the kind of imprecision that used to be merely embarrassing and is now actionable. The short version is that they have been preparing for this moment since approximately 1976, that almost no-one has been listening, and that we are now going to need them rather urgently and at scale. The longer version, which is the rest of the essay, contains some jokes at the expense of the present author, who has written more than one prompt that began “You are a helpful assistant” and is in no position to be smug.
The pedants you are about to need
There exists, and has existed for some time, a small and dignified community of people who have spent their careers on the question of how to write a sentence precise enough that a computer cannot misread it. They publish in journals you have not heard of. They use phrases like “fact type” and “deontic operator” without any visible embarrassment. They have, between them, produced an OMG specification called SBVR (Semantics of Business Vocabulary and Business Rules, 2008, and yes the acronym is what it is), a guidance system called RuleSpeak (Ron Ross, who has been quietly insisting on the phrase the system must into a largely indifferent void since the 1980s), an academic project at the University of Zurich called Attempto Controlled English, and a body of work in legal drafting that runs all the way back to George Coode’s On Legislative Expression in 1845 and which has, broadly, been ignored by every parliamentary draftsman who came after him.
These people have already had the argument we are about to have. They have already worked out that “promptly” is not a deadline, that “where appropriate” is what one writes when one has not, in fact, decided, and that any sentence containing the words “use your judgement” is not strictly speaking an instruction. They have written it down. They have published the books. The books were about to go out of print.
We are about to need these people. They are going to say “I told you so” in a controlled vocabulary, and they will be entirely within their rights.
What’s actually changed
It is worth being precise about what is new, because the temptation is to say everything and the truth is almost nothing, but in an important place.
The classical pipeline of the business rules world ran like this: a human wrote a rule in controlled English, the controlled English was translated β by a tool, or a person, or a tool supervised by a person β into a formal representation in some flavour of logic, and the formal representation was what actually ran. The English was a surface. It existed so that humans could read it, argue about it, sign it off, and put it in a binder. The logic was the operative artefact. When the system did something, it did the thing because the logic said so, not because the English said so.
Large language models invert this. The language is the operative artefact. The agent reads your prompt and acts; there is no intervening logical representation that you wrote, that you can inspect, or that you can be held to. The formalism, if it exists at all, is now a thing you build afterwards, to audit what happened, to test what might happen, or to constrain what will be allowed to happen next.
This is the move that has not been adequately appreciated. We have not abolished the need for linguistic precision. We have moved the place where it has to live. It used to live in the formalism, where it was enforced by a compiler that would simply refuse to run if you got it wrong. It now lives in the English, where it is enforced by β and I want you to sit with this for a moment β your own discipline as a writer of English on a Thursday afternoon when you are also trying to do four other things.
This is, somewhat, the problem.
The bit about being asked, by name
The EU AI Act presupposes that you can document what your system was instructed to do. The FCA’s Consumer Duty presupposes that someone, somewhere, can be asked why a particular customer got a particular outcome. The Senior Managers and Certification Regime has, over the last decade, made the question which named human? a regulatory primitive in financial services. NIST’s AI Risk Management Framework asks, with a straight face, that AI behaviour be “measurable” and its instructions “documented”. All of this is built on top of an assumption β quaint, in retrospect β that the instruction given to a system is a thing you can produce in court.
The instruction given to your system is agent-prompt-v3-FINAL-actually-final.md. It begins, “You are a helpful assistant.”
It begins, “You are a helpful assistant.”
I am repeating the line because I want you to hear it the way External Counsel is going to hear it. You are a helpful assistant. This is the substrate on which we have built an accountability regime. You are a helpful assistant. This is the artefact a regulator is going to be invited to inspect. You are a helpful assistant. This is what you wrote, on a Thursday, in a hurry, six months ago, and which has now done something that has caused four people to spend an afternoon in a room with you.
“But regulations are full of ‘reasonable’ and ‘promptly'”
Yes. They are. And it is not an accident.
Lawyers and regulators have a term of art for this: the standard, as opposed to the rule. A rule is decided in advance β speed limit 30mph, retention period seven years. A standard is decided after the fact β reasonable care, prompt response, fair treatment. The vagueness is deliberate. It denies bad actors a bright line to game right up to. It allows the regulation to travel into circumstances the drafter could not have anticipated. And, most importantly, it transfers the interpretive labour onto you. When the FCA writes “act to deliver good outcomes for retail customers”, it is not failing to be precise. It is requiring you to be precise, on its behalf, in your specific context, and to be ready to defend your interpretation when asked.
In the pre-agent world, you had a workforce who did this for you. Underwriters, claims handlers, compliance officers β people who had absorbed, through years of training and case-by-case experience, what their firm meant by “reasonable” in their context. That tacit interpretive competence was the layer between the regulator’s deliberately open-textured standard and the day-to-day decisions taken in its name. It mostly wasn’t written down, because it didn’t have to be. It lived in the people.
Agents do not have that tacit competence. They have your prompt. The interpretive layer that used to live, unwritten, in the heads of experienced staff now has to be written down and given to the agent, because the agent has nowhere else to get it from.
The regulator is still allowed to say “reasonable”. You no longer are. Not because “reasonable” is a bad word, but because the entity downstream of you, which used to be a human who knew what you meant, is now a system that doesn’t.
The five things you have to control
There are, when the dust settles, five things you have to control if a sentence is going to be safe to put in front of an autonomous system. They are not novel and they are not mine. Most of them are in the SBVR specification, the rest are in any decent textbook on legal drafting, and the whole edifice has been sitting in plain sight for years while the rest of us were busy discovering, with the air of pioneers, that prompts work better when you are nice to them.
What you say. A controlled vocabulary, applied with humourless consistency. If the thing is a “loan application”, it is a loan application in every sentence that mentions it. It is not, in paragraph four, a “case”. It is not, in paragraph seven, “the request”. It is not, in the bullet list near the bottom that someone added in a hurry, “the submission”. This sounds trivial. It is the single most violated rule in every prompt I have ever audited, including, I should say, several of my own. The agent, being helpful, infers that “case” and “request” must be different things, since you have gone to the trouble of using different words for them, and you now have a referential ambiguity sitting in production which is going to cost someone their bonus.
The same goes, more sharply, for vague predicates. “Promptly” is not a deadline β until you make it one. “Reasonable” is not a criterion β until you make it one. “Where appropriate” is what one writes when one has not, in fact, decided.
What you mean. Behind every controlled vocabulary is a fact model: the nouns, the verbs, the relationships between them, the values an attribute is permitted to take. SBVR calls these noun concepts, verb concepts and fact types, and treats them as logically prior to any rule. The rest of us tend to treat them as something the developers will sort out later, and the developers tend to treat them as something the analysts will sort out later, and the eventual result is the well-known industrial phenomenon in which six teams use the word “customer” to mean six different things and only discover this in production, on a Friday, in front of a regulator.
What kind of statement it is. There is a substantial difference, both linguistic and operational, between a definition (“a ‘closed’ application is one whose status is Closed”), a structural constraint (“an application has exactly one applicant”), an operational rule (“if the score is below the threshold, reject”), and an instruction with exceptions (“approve, unless a fraud flag is set, unless the fraud flag was set by the same agent within the previous hour, unless⦔). These look almost identical in English. They behave very differently when something goes wrong. RuleSpeak’s particular contribution here, for which Ron Ross has not been adequately thanked, is the dull but load-bearing observation that an operational rule should always begin with the subject and the modal verb: the system must, the underwriter may, a closed application must not. You may find this stylistically unbearable. It is, nevertheless, correct.
In what mode. This is the bit where I have to apologise for an earlier draft of this material in which I used the word “modality” to mean approximately four different things, in the manner of a teenager using “literally”. The useful flavours are four. Deontic: must, may, must not β the world of obligations and permissions, where most rules live. Alethic: necessarily, possibly β the world of structural truths, where every application has exactly one status not because we have decided so as a matter of policy but because it is incoherent for it to be otherwise. Temporal: by when, for how long, after what β the world in which “respond promptly” is replaced by something a clock can adjudicate. Defeasible: normally, unless, except where β the world in which a rule is allowed to admit, honestly, that it has exceptions, without having to enumerate them all on the day it is written. The sentence “All applications must be reviewed within two business days unless they have been flagged for fraud” contains a deontic must, a temporal within two business days, and a defeasible unless, and if your instruction does not distinguish them, neither will the thing reading it. It will pick one. You will not, in advance, know which.
Under what conditions it counts. Here is where SBVR and RuleSpeak begin to thin out, and where I would gently suggest most of the actually interesting work for the next decade is going to be done. A rule is not just a statement. It is a statement that applies under some conditions and not others. It applies in this jurisdiction and not that one. It applies from this date and not before. It applies on the authority of a named person, or it does not. It is supported by evidence which is itself dated, sourced, possibly stale. It outranks some other rule, or is outranked by it, and somebody, somewhere, has decided which. These are the questions you are going to be asked, in the meeting from the cold open. Which version of the policy was the agent operating under at 3.47pm on the eleventh? Who authorised that version? On what evidence? Did it conflict with the consumer-credit guidance issued the previous Tuesday, and if it did, which one was supposed to win, and why? If your instruction contains no answer to these questions, the answer will be supplied for you, in retrospect, by the most expensive person in the room.
What currently passes
What currently passes for the discipline of writing instructions for autonomous systems, in 2026, is as follows.
There is a Notion page. The Notion page is called something like Agent Instructions (Master). It has been edited 47 times, most recently by a person who has since left the company. It contains a paragraph that begins “You are a helpful assistant”. It contains a list of bullet points, some of which are imperatives, some of which are observations, and at least one of which is a half-finished sentence that nobody has had the heart to delete. It has no version history beyond what Notion provides by accident. It does not say which version of itself was running on any particular day. It does not say who authorised it. It does not say what it overrides or is overridden by. It does not say where it applies. It contains the word “robust” four times.
We let people draft these documents with less rigour than we require of a junior solicitor drafting a clause in a tenancy agreement about a fridge. The war on error has, on this front, not yet begun.
What good looks like
The alternative is not beautiful. It looks something like this:
Effective from 1 June 2026. Applies to UK consumer-credit loan applications under FCA CONC. Authorised by [named individual], Head of Underwriting Policy. Supersedes Rule Set v2 (effective 1 January 2026 to 31 May 2026).
Definitions. A loan application is a record submitted via the customer portal whose status takes exactly one value from {Submitted, UnderReview, Approved, Rejected, Closed}. A fraud flag is a record created by the upstream fraud service and attached to a loan application. For the purposes of this rule set, “promptly” means within two business days unless otherwise stated.
Rules. (1) The system must move every Submitted loan application to UnderReview within two business days of submission. (2) The system must not move a loan application to Approved while an unresolved fraud flag is attached to it. (3) Where a loan application has a credit score below 580, the system should reject the application β unless the application has supplementary income evidence verified within the previous 90 days, in which case the system must escalate the application to a human underwriter. (4) Only a user with role Senior Underwriter may override a Reject decision; each override creates an audit event recording the user, the application, and the timestamp. (5) Where this rule set conflicts with FCA CONC 5.2A, FCA CONC 5.2A prevails.
That is the same instruction. It is shorter than the Notion page. It is duller than the Notion page. It is not going to win any prizes for prose. Every sentence in it can be pointed to in a meeting and answered for. Every term in it means one thing. Every rule begins with the subject and the modal verb, in the manner of Mr Ross, and admits of exceptions where exceptions are admitted. The vague word the regulator is allowed to keep β “promptly” β has been pinned down, in this firm, in this product, on this date, by a named person, to mean a specific thing. It has a date, an authority, and a tie-breaker.
The point is not that this is good writing. The point is that it is answerable writing β writing you can be asked about, by a regulator, six months later, and have something to say.
Almost there…..
The discipline I am describing is unglamorous. The audience for it is small. The prior art is decades old and largely unfashionable, and most of its practitioners have moved on to more remunerative consulting work or to retirement. The phrases I have been throwing around β fact type, deontic operator, defeasible rule β are not going to trend. They are not going to appear on a conference T-shirt. They are not going to be the subject of a Netflix documentary in which a charismatic founder explains, against a backdrop of rolling hills, how he reinvented logic.
The alternative, however, is being deposed about a sentence you wrote in a hurry on a Thursday.
We are about to discover, I think, that the most consequential combatants in the war on error may turn out to be the pedants. Not the model architects. Not the prompt-whisperers. The pedants β the people who have spent their careers caring, with an intensity that has at times verged on the eccentric, about the difference between must and should, between case and application, between a rule that applies and a rule that holds. You should hope you are one. Or know one. Or, at the very minimum, be on speaking terms with one.
The alternative is a man with a lanyard, charging by the minute, asking you what you meant.
| Sub-control | Informal name | Example | Formal cue |
|---|---|---|---|
| 1. What you say (lexical and syntactic control) | |||
| Controlled vocabulary | Approved terms | Use “loan application”, not “case”, “request”, or “submission” | LoanApplication(x) |
| Lexical precision | No vague predicates | “within 2 business days”, not “promptly” | Submitted(x,t) β DueBy(x, t+2bd) |
| Enumerated value domain | Closed lists | status β {Submitted, UnderReview, Approved, Rejected, Closed} | Status(x,s) β s β {β¦} |
| Canonical clause pattern | Subject + modal verb | “The system must validate the application” | System(s) β§ Application(a) β O(Validate(s,a)) |
| Atomic statement | One rule per sentence | “The system validates identity” β not three things in a trench coat | Application(a) β ValidatesIdentity(System,a) |
| Anaphora control | Clear references | “the application”, not “it” | resolve it β Application(a) |
| Attachment control | Clear modifier scope | “Reject applications that have fraud flags” β not “Reject applications, which have fraud flags” | Application(a) β§ HasFraudFlag(a) β Reject(a) |
| 2. What you mean (semantic grounding) | |||
| Noun concept | Map nouns to entities | Applicant, Application, FraudFlag | Applicant(x), Application(x) |
| Verb concept / fact type | Map verbs to relations | “applicant submits application” | Submits(applicant, application) |
| Attributeβvalue grounding | Map adjectives to fields | “rejected application” | Status(a, Rejected) |
| State-transition grounding | Map life-cycle verbs to state changes | Submitted β UnderReview β Approved | State(a, Submitted, t) β§ StartReview(a, t) β State(a, UnderReview, t+1) |
| Cardinality | Say how many | “Each application has exactly one applicant” | βa (Application(a) β β! p HasApplicant(a, p)) |
| 3. What kind of statement it is (rule form) | |||
| Definition | “X means Y” | “A ‘closed’ application is one whose status is Closed” | Closed(a) β Status(a, Closed) |
| Structural constraint | Holds by structure, not by policy | “An application has exactly one status” | β‘ βa (Application(a) β β! s Status(a, s)) |
| Operational rule | Ifβthen conduct rule | “If score < threshold, reject” | Score(a, s) β§ s < Threshold β O(Reject(a)) |
| Rule with exception | Override logic | “Approve, unless a fraud flag is set” | Eligible(a) β§ Β¬FraudFlag(a) β Approve(a) |
| Contract-style rule | Pre- and post-conditions | Pre: Submitted(a) β§ Eligible(a); Post: Approved(a) | {Submitted(a) β§ Eligible(a)} Approve(a) {Approved(a)} |
| 4. In what mode (logical modality, properly so called) | |||
| See Table 2. | |||
| 5. Under what conditions it counts (governance and rule context) | |||
| Jurisdictional validity | Where it applies | “Applies under FCA CONC” | Applies(r, a) β UKConsumerCredit(a) |
| Effective date | When it applies | “Rule v3 applies from 1 June 2026” | t β₯ 2026-06-01 β Applies(RuleV3, t) |
| Authority | Who said so | “Authorised by Head of Underwriting Policy” | Authorises(HeadOfUW, RuleV3) |
| Norm priority | Which rule wins | “FCA CONC 5.2A overrides internal Rule v3” | Priority(CONC_5_2A, RuleV3) |
| Actor capacity | Role-based powers | “Only a Senior Underwriter may override a Reject” | Override(u, a) β SeniorUnderwriter(u) |
| Consent / authorisation basis | Permission to act on data | “Process data only if consent is recorded” | ProcessData(x, d) β RecordedConsent(x, d) |
| Evidence basis | What supports the decision | “Decision must be supported by verified income evidence” | Decision(d, a) β βe (Verified(e) β§ Supports(e, d)) |
| Data quality | Fitness of evidence | “Evidence verified and < 90 days old” | Usable(e, t) β Verified(e) β§ Age(e, t) < 90d |
| Observability | Detectability of action | “Each override creates an audit event” | Override(u, a, t) β βe (AuditEvent(e) β§ Records(e, Override(u, a, t))) |
| Remediation | What happens when things break | “If validation fails, return for correction” | ValidationFails(a) β ReturnForCorrection(a) |
| Lifecycle phase | What’s allowed when | “A closed application must not be edited” | Closed(a) β O(Β¬Edit(a)) |
| Concurrency / mutual exclusion | What can’t co-exist | “Cannot be both Approved and Rejected” | Β¬(Status(a, Approved) β§ Status(a, Rejected)) |
| Triggering event | What sets the rule running | “When payment fails, suspend the account” | PaymentFailed(acct, t) β Suspend(acct, t+1) |
| Goal / preference | What we’re optimising for | “Minimise wrongful approvals” | Minimise |{a : Approved(a) β§ ShouldReject(a)}| |
| Modality | Logic family | Informal name | Example | Formal cue |
|---|---|---|---|---|
| Deontic | Deontic logic (von Wright, SDL) | Must / may / must not | “The system must reject fraudulent applications” | Fraudulent(a) β O(Reject(System, a)) |
| Alethic | Modal logic (S5 for structural truths) | Necessarily / possibly | “Each application necessarily has exactly one status” | β‘ βa (Application(a) β β! s Status(a, s)) |
| Temporal | Temporal logic (LTL / metric) | By when, until, after | “Respond within 2 seconds of receipt” | Request(x, t) β β t' (Response(x, t') β§ t' β€ t + 2s) |
| Defeasible | Defeasible / non-monotonic logic | Normally, unless, except where | “Normally approve eligible applications, unless a fraud flag is set” | Eligible(a) β§ Β¬FraudFlag(a) β Approve(a) |
| Epistemic | Epistemic logic | What is known, what is unknown | “Eligibility is unknown until evidence is verified” | Β¬Verified(e) β Β¬K(Eligible(a)) |
| Probabilistic | Probability / Bayesian | Likelihood, confidence | “Approve if fraud probability < 0.05” | P(Fraud(a)) < 0.05 β Approve(a) |
| Evidential | Evidential / justification logic | Supported by, on the authority of | “Decision must be supported by verified income evidence” | Decision(d, a) β βe (Verified(e) β§ Supports(e, d)) |
Further Reading:
The standard
SBVR (Semantics of Business Vocabulary and Business Rules), OMG Specification, current version 1.5. The formal artefact itself, available at omg.org/spec/SBVR/Current. It is, fair warning, written in the prose of an OMG specification, which is to say in the prose of an OMG specification. Read the annexes first; they’re more humane than the body. The “Structured English” notation is the bit most people actually want, and it lives in Annex C. OMG
The practitioner literature
Ronald G. Ross, Business Rule Concepts: Getting to the Point of Knowledge, 4th edition, Business Rule Solutions, 2013. The short, readable one. If you read only one Ross book, this is it.
Ronald G. Ross, Principles of the Business Rule Approach, Addison-Wesley, 2003. The longer, more architectural one. Part III is the original RuleSpeak primer. The book “provides a comprehensive language, called BRS RuleSpeak, to capture and express your business rules”, in the author’s own slightly stately phrasing. Amazon
Ronald G. Ross and Gladys S.W. Lam, Building Business Solutions: Business Analysis with Business Rules, 2nd edition, 2015. The applied one β what the discipline looks like inside an actual business analysis engagement.
The Business Rules Manifesto (Business Rules Group, 2003). Two pages. Free. Twenty-odd numbered propositions which read like a slightly grumpy charter and which have aged remarkably well. Available at businessrulesgroup.org.
BRCommunity.com β Ross’s Business Rules Journal, online and free, archives going back to 2000. The 2024 Ross essays β The Five Basic Skills of Discovering and Expressing Rules, The Urgent Need for New Rule Platforms in Business and Government, Being Unambiguous Beyond Reasonable Doubt in Expressing Rules β are particularly to the point of this post, and free to read. Brcommunity
Requirements Engineering
Axel van Lamsweerde, Requirements Engineering: From System Goals to UML Models to Software Specifications, Wiley, 2009. The canonical text on KAOS and goal-oriented requirements engineering β how to derive the rules from the goals they’re meant to serve, rather than just writing the rules.
The CNL canon
Norbert E. Fuchs, Kaarel Kaljurand and Tobias Kuhn, Attempto Controlled English for Knowledge Representation (in Reasoning Web, Springer LNCS 5224, 2008). The standard introduction to “a controlled natural language, i.e. a precisely defined subset of English that can automatically and unambiguously be translated into first-order logic”. The Attempto group at Zurich are the people who actually built the thing. Springer
Tobias Kuhn, A Survey and Classification of Controlled Natural Languages, Computational Linguistics 40(1), 2014. The map of the territory. If you only read one survey, read this one β Kuhn classifies every CNL of any consequence on a four-dimensional grid (PENS: Precision, Expressiveness, Naturalness, Simplicity) and the result is genuinely clarifying.
Rolf Schwitter (Macquarie) on PENG (Processable English) β see his 2010 paper Controlled Natural Languages for Knowledge Representation in COLING. The other major academic CNL tradition, alongside Attempto.
George Coode, On Legislative Expression, 1845. Free on archive.org. Yes, 1845. Coode worked out most of what RuleSpeak would later rediscover, in the context of drafting Acts of Parliament, and his four-part scheme (case, condition, subject, action) is essentially the canonical rule sentence with a different vocabulary. Worth reading once just to be properly humbled.
What’s happening right now (2026)
Five papers from this year, all on arXiv, all directly on the thesis of the post: how to put a formal layer between natural-language instructions and an autonomous system, so that someone can be asked about it later.
Liu, Zhang et al., Explicating Tacit Regulatory Knowledge from LLMs to Auto-Formalize Requirements for Compliance Test Case Generation (arXiv 2601.09762, January 2026). The RAFT framework. Almost embarrassingly on-topic for this post: “compliance testing in practice remains predominantly manual. Domain experts are required to interpret lengthy and complex regulatory texts and translate them into executable test cases”, and they propose using LLMs to extract the tacit interpretive layer I was banging on about in the “reasonable” and “promptly” section. Whether their method works is a separate question; that someone is asking it formally is the encouraging thing. arxiv
Anonymous (under review for ICSE 2026), Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications (arXiv 2604.18228, April 2026). Tackles head-on the gap between informal specifications and formally verifiable properties: “recent Large Language Model (LLM)-based approaches can generate formal artifacts from text, they mainly focus on syntactic correctness and do not ensure semantic alignment between informal requirements and formally verifiable properties”. Which is, I think, the cleanest one-sentence statement of the actual problem you’ll find anywhere. arXiv
Bhardwaj, Agent Behavioral Contracts: Formal Specification and Runtime Enforcement for Reliable Autonomous AI Agents (arXiv 2602.22302, February 2026). The most ambitious of this year’s crop. Imports Hoare-logic-style preconditions, invariants and postconditions to LLM agents, with probabilistic compliance guarantees and a “Drift Bounds Theorem”. Whether you buy the theorem is a matter for the comments section; the direction β contracts for prompts β is the right one.
Wang et al., AgentSpec: A Customizable Runtime Enforcement Framework for LLM Agents (ICSE 2026). A rule-based DSL for specifying what an agent may and may not do, enforced at runtime. Effectively RuleSpeak for agents, forty years on. The paper is in the ICSE 2026 proceedings; preprint on arXiv.
Lou et al., FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight (arXiv 2602.11136, February 2026). Uses LLMs as “specification compilers” β the LLM extracts atomic facts from an agent’s trajectory, an SMT solver checks them against a formal specification. “Agents guided by Dafny specifications improve from 70.7% to 99.8% accuracy over three rounds, while all LLM-as-a-Judge baselines show no improvement or degradation”. The numbers should be read with appropriate scepticism, but the methodology is the interesting bit: oversight with a logic underneath it, rather than oversight by another LLM nodding along. arxivarxiv
