Regulation often follows a familiar pattern. A new technology creates a new kind of risk. Something goes wrong, the harm becomes visible, and the law evolves in response.
Healthcare offers a clear example. In 1937, an untested liquid drug called Elixir Sulfanilamide killed more than 100 people, many of them children. The disaster helped drive the passage of the Federal Food, Drug, and Cosmetic Act the following year. As technology changed, regulation changed with it. The Medical Device Amendments of 1976 expanded federal oversight of medical devices, and decades later the 21st Century Cures Act clarified which software functions should and should not be treated as medical devices.
The pattern matters because liability often appears before regulation fully catches up.
AI agents are creating the next version of this problem. They can disclose sensitive information, make promises to customers, contact people at restricted times, approve actions, or communicate information that creates legal consequences. Many of the obligations governing those actions already exist, even if the law never uses the words “AI agent.”
The challenge is figuring out, in production, whether each action an agent takes complies with those obligations.
Why another LLM is not enough
State-of-the-art models can interpret complex text and perform sophisticated reasoning. They are also probabilistic: the same input can produce different answers, explanations, and reasoning paths across separate runs.
That creates a problem for compliance. After something goes wrong, a company needs to reconstruct what the agent did, which facts mattered, which legal requirement applied, whether an exception applied, why the system reached its verdict, and which interpretation of the law was active at the time.
An LLM can generate a convincing explanation for all of this. A convincing explanation alone does not establish that the conclusion followed the legal logic the system was supposed to apply.
Prompt engineering can improve reliability. Compliance requires an additional layer of control: a reproducible and mechanically checkable path from the applicable law, to the relevant facts, to the final verdict.
A company should be able to explain why an interaction was considered compliant or non-compliant, rather than simply producing a plausible answer.
Use the LLM to identify the facts
At Ollive, we narrow the role of the runtime LLM. Its job is to understand what happened and extract the facts that matter, that’s it.
We first break each regulation into smaller, machine-readable pieces that we call directives. Each directive captures one specific legal requirement and defines the facts needed to evaluate it.
A directive may represent:
- an obligation, something the agent must do;
- a prohibition, something the agent must not do;
- a permission, something the agent is allowed to do; or
- an exception, a condition under which the normal requirement changes.
Consider a simplified example.
Suppose a directive says that a debt collection agent must not contact a consumer before 8 a.m. in the consumer’s local time unless that consumer has said an earlier time is convenient.
An AI collections agent places a call at 7:30 a.m. The customer record contains an old note saying, “Call before work.” It also contains a more recent instruction saying, “Do not call before 9 a.m.”
The LLM extracts the relevant facts:
- the consumer’s local time was 7:30 a.m.;
- the consumer had previously allowed earlier calls;
- the consumer later withdrew that permission; and
- the later instruction was active when the call occurred.
Those facts are passed to the relevant directive, which evaluates them using the legal interpretation already encoded into the system.
If an important fact is missing, such as the consumer’s timezone, the system should preserve that uncertainty. It can return an indeterminate verdict and ask for more evidence instead of silently assuming compliance.
This creates a clean separation of responsibilities. The LLM identifies what happened. The directive evaluates those facts against a defined interpretation of the law.
What formal verification adds
We use Lean 4 to make the directive layer mechanically checkable.
Lean is a programming language and proof assistant. It checks whether a conclusion follows from the definitions, assumptions, and facts supplied to it.
This matters because natural-language reasoning can skip an assumption or make a logical jump while still sounding persuasive. Lean checks the underlying logic directly.
The guarantee is deliberately narrow:
Given this interpretation of the law and these facts, this verdict follows from the directive we encoded.
That is the level of certainty formal verification can provide.
Lean also helps us check that the compliance system behaves the way we intended. For example, we can verify that:
- the same facts are evaluated using the same directive;
- an exception is applied only when its required conditions are present;
- missing information cannot silently become a definite verdict; and
- the verdict shown to the user comes from the directive the system says it used.
This gives us confidence that the software is consistently applying the legal logic we encoded.
It also creates something more useful than a natural-language explanation. The system can show exactly how a verdict follows from an explicit legal interpretation.
Building the legal model
The legal specification evolves through repeated testing and review.
For a given legal obligation, we can ask two independent systems to translate the same source text into a directive. When the directive depends on a manageable number of yes-or-no facts, we can test both versions across every relevant combination of those facts.
Suppose a directive depends on four (N=4) binary facts. There are 16 (2^N) possible combinations. We can run both versions across all 16 and see exactly where their verdicts differ.
Imagine the two versions agree almost everywhere but disagree on one scenario:
- the call happened before 8 a.m.;
- the consumer had previously allowed early calls;
- the consumer later withdrew that permission; and
- the withdrawal was stored in a different system.
One version says the call was permitted. The other says it was prohibited.
That disagreement gives a human reviewer a concrete question to resolve.
It may reveal that one system misunderstood the source text, an important condition was left out, the directive was implemented incorrectly, the two systems disagree about which evidence should take priority, or the law itself is genuinely ambiguous.
A human reviewer then examines the underlying legal text and decides how the directive should handle that scenario.
Once the interpretation is settled, we record the decision and update the directive. We also save the factual scenario as a regression test. If the directive is later changed, the system automatically checks whether that previously settled scenario still produces the expected verdict.
Then we compare the independent versions again.
Over time, this process removes accidental disagreements and surfaces the legal questions that genuinely require judgment.
Some ambiguity should remain visible
Legal questions do not always have a clean answer. Facts may be incomplete, regulations may overlap, and reasonable interpretations can differ.
When the underlying law is unclear, the system should preserve that uncertainty. A verdict such as “indeterminate, human review required” may be the correct outcome.
Formal verification helps make those boundaries explicit. Lawyers and subject-matter experts remain responsible for deciding how a provision should be interpreted, while the system records those decisions and applies them consistently.
The aim is to make uncertainty visible and traceable instead of leaving it buried inside a prompt or model response.
The Path to a Defensible Verdict
The end result is a reproducible path:
regulation → recorded interpretation → directive → observed facts → verdict
Each step can be inspected. Interpretations can be versioned, directives can be tested, and verdicts can be traced back to the facts and legal reasoning that produced them.
That becomes especially important after something goes wrong.
A customer, regulator, insurer, or court may ask why the system considered a particular interaction compliant. The company should be able to show which directive applied, which facts were observed, which interpretation sat behind it, and how those inputs produced the verdict.
“The model thought it was okay” will rarely be a satisfying answer.
AI is extremely useful for understanding messy, unstructured behaviour. It can read conversations, actions, system logs, and context, then convert them into structured facts.
Evaluating those facts against a legal requirement calls for a different kind of system. The directive should be explicit, testable, versioned, and mechanically checked, with humans responsible for resolving legal ambiguity.
This architecture makes compliance decisions easier to trace, reproduce, and defend. For AI agents operating in regulated environments, that level of clarity matters far more than another confident answer.