Abstract
When a large language model is asked to act on a user's behalf — book a flight, approve a payment — the designer must constrain what the model is allowed to say so it matches what the rest of the system is prepared to act on. This paper maps the middle layer between the model and the executing system: the ontology control layer that turns free-form text into structured, validated, actionable commands. It lays out a four-axis design space and four reference architectures (Prompt-Bound, Schema-Bound, Grammar-Constrained, and Verified Mediator), an honest accounting of what each can and cannot formally prove, and a survey of the formal methods themselves — with particular attention to the B method — framed around five concentric rings of verifiability. An agentic-payment example runs throughout.
Executive summary
When a large language model is asked to take actions on a user's behalf — book a flight, approve a payment, schedule a procedure — the system designer faces a question with surprisingly few satisfying answers: how do you constrain what the model is allowed to say, in a way that matches what the rest of the system is prepared to act on?
This paper maps the space of answers. The middle layer between the language model and the executing system — the layer that converts free-form text into structured, validated, actionable commands — is the ontology control layer, where ontology is used in the technical sense: a structured description of the entities a system deals with (counterparties, currencies, purposes, time windows), the relationships between them, and the rules they must collectively satisfy.
The contribution is fourfold:
- A four-axis design space that any control architecture sits somewhere within.
- Four named reference architectures — Prompt-Bound, Schema-Bound, Grammar-Constrained, and Verified Mediator — the most coherent points in that space.
- An honest accounting of which properties of each architecture can be formally proved, which cannot, and where the line between engineering and research falls.
- A survey of the formal methods, with particular attention to the B method (used to prove the Paris Métro Line 14 signalling system) and its operationalisation for an LLM mediator.
Formal verification runs through the paper as a transverse theme: the question "is this verifiable?" has a different answer at every layer of the stack. The paper names five concentric rings of verifiability and draws a clear line between the engineering side (schema soundness, validator totality, system safety invariants — all tractable today) and the research side (whether a model truly understands the user, and whether the system end-to-end does the right thing). An agentic-payment illustration carries the argument from design space to worked example.