AI agents and MCP: admission comes from the compiler, not from the model’s text

A language model is good at turning a discussion into a draft rule and good at explaining a result in words. It is not fit to be the final arbiter: its answer is probabilistic, and how convincing a text sounds has nothing to do with whether it is right. “The order is ready, go ahead and ship” is not an admission, it is a hypothesis. A separate step turns it into an admission: evaluating a claim on real data, with two outcomes and a clear reason on refusal.

This chapter is about building that step around flang and about where the responsibility of the agent, the compiler and the application begins and ends.

Minimal example

The rule and the lookup of an order by number — a complete program; it passes the check and both promises are proved:

модуль «Исполнение заказа»

объект «Заказ»
  «номер»: строка
  «оплачен»: признак
  «склад подтвердил»: признак

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
  обеспечивает «без подтверждения склада не отгружается» если не заказ.«склад подтвердил» то результат равен нет иначе да
  пример «оплаченный и подтверждённый можно»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да и «склад подтвердил» равным да
    ожидается да
  если заказ.«оплачен»
    то заказ.«склад подтвердил»
    иначе нет

тотальная функция «Заказ с номером отгружается»
  принимает заказы: список «Заказ», номер: строка
  возвращает признак
  пример «заказа нет в данных — отгрузки нет»
    дано заказы равно пустой список
    дано номер равно "ЗК-0000"
    ожидается нет
  разбор (отфильтровать заказы где заказ → заказ.«номер» равен номер)
    случай пусто
      то нет
    случай голова и хвост
      то «Можно отгрузить» от голова

The facts are an ordinary JSON snapshot of data, not part of the program:

{
  "номер": "ЗК-7781",
  "заказы": [
    { "номер": "ЗК-7781", "оплачен": true, "склад подтвердил": true }
  ]
}

The claim that decides admission is one line:

flang facts shipment.flang --facts facts.json \
  --claims '["«Заказ с номером отгружается» от заказы, номер равно да"]'

What the compiler does

The check takes three independent steps, and each gives its own answer.

flang check parses the program, checks types and names, proves that every function terminates and runs the examples. A field, variant or function that does not exist gives FLANG_UNKNOWN_NAME; an example that does not match gives FLANG_EXAMPLE.

flang check --proof adds the proof report: which promise is proved for all inputs, which is checked only on examples (“сетка N”, grid N) and which is merely stated. Exit code 0 means everything is proved, 3 means not everything.

flang facts evaluates a claim on facts and answers in JSON:

{"ok":true,"results":[{"claim":"«Заказ с номером отгружается» от заказы, номер равно да","holds":true,"why":"«Заказ с номером отгружается» от факта «заказы», факта «номер» = да; требование «равно да» выполнено","steps":[…],"status":"verified"}]}

steps lists what was taken from the facts, what the function returned and what it was compared with. The status comes in three kinds: verified — the claim holds, refuted — evaluated and does not hold, refused — could not be evaluated (a fact is missing, the function is missing, a fact has the wrong type). Exit code 1 for refuted and refused means “no”, not a tool failure.

flang facts may call total functions only. Without the тотальная (total) mark the answer reads:

функция «Заказ с номером отгружается» не помечена как «тотальная»; факт-чекинг допускает только тотальные функции — иначе ответ может не наступить

The loop: proposal → check → admission → effect

1. The agent proposes a rule — a flang program — or collects facts.
2. The compiler checks the program: types, termination, examples, proofs.
3. A person accepts the rule into the repository, like any other code.
4. On the production path the application evaluates a fixed claim on facts (flang facts) and gets “yes” or “no” with a reason.
5. The application performs the effect — only on “yes”.

The effect is always outside. A flang function cannot ship an order, charge money or send an email: an action in the language is a described value that whoever runs the program executes. The agent cannot “accidentally” ship an order through the check, because the check has no such ability at all. The most it can achieve is allowed: true where the facts support it.

MCP tools

flang --mcp-mode is a service for an AI assistant: JSON-RPC over the standard streams, one message per line. It goes into the assistant’s settings like this:

{"mcpServers": {"flang-validator": {"command": "flang", "args": ["--mcp-mode"], "env": {}}}}

There are two tools:

claim for flang_prove is the name of a promise from an обеспечивает «имя» … line.

The key property of these answers: they have no “ok” field. The three verdicts — “proved”, “grid N” and “stated, not proved” — are reported separately, and every answer starts with a dictionary of these words. The answer of flang_prove on the model from chapter 9 begins like this:

Слова ведомости, и они НЕ взаимозаменяемы:
  «доказано» — утверждение обо ВСЕХ входах, выведенное из объявлений и структуры;
  «доказано индукцией по «Т»» — то же обо всех входах типа «Т»;
  «сетка N» — посчитано на N значениях автора. ЭТО НЕ ДОКАЗАТЕЛЬСТВО;
  «объявлено, не доказано» — утверждение высказано, доказательства при нём нет;
  «НАРУШЕНО» — ложь, уже найденная примером автора.
Ни одно из этих слов не сводится к «ок».

A program that fails the check gets a separate answer: “the program did NOT pass the language check, so the proof report is not printed” — followed by the error code. The protocol itself carries no error flag, so the client reads the text of the verdict, not just the fact that the call succeeded.

What the MCP service lacks: evaluation on facts. flang facts is a command of the binary, not a tool of the service. That is right for the loop: the agent may check a rule on its own, while admission on data comes from the application.

The service reads no files and makes no network calls: the program arrives as an argument of the call. This is no protection against prompt injection, but it is a smaller surface: the tool the agent calls most often physically cannot read the disk or change state.

The agent collects facts, not program text

Generating a program as text always leaves room for a mistake: a wrong quote, a lost indent, a stray line. The compiler will catch it, but on the production path it should not happen at all. So the roles are split like this:

• the program and the claim live in the repository and have passed review;
• the agent chooses what to ask about: the order number, the data snapshot;
• how to ask is decided by the application code.

A flang program cannot be built from JSON: flang ast turns a program into JSON, but the compiler has no road back. So everything that comes from the agent at run time must come as data — facts for flang facts.

The claim is not given to the agent either. If the agent chose the --claims string, it could ask “… equals no” and get an honest verified — on an order that must not be shipped:

«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет; требование «равно нет» выполнено

The compiler is right here: the claim does hold. The mistake would be that the application asked the wrong question.

The guard in code

A working example lives in the course repository: examples/spec/shipment-guard/guard.mjs. The claim is a module constant; the order number and the data snapshot go into the facts:

export const CLAIM = '«Заказ с номером отгружается» от заказы, номер равно да';

export async function decideShipment(orderNumber, orders) {
  const verdict = await (await flang()).facts(MODEL_FILE, { заказы: orders, номер: String(orderNumber) }, [CLAIM]);
  const [result] = verdict.results;
  return { allowed: verdict.ok && result.holds === true, claim: CLAIM, why: result.why, steps: result.steps ?? [] };
}

flang() takes the flang binary if the FLANG_BIN variable is set, otherwise the same compiler built to WebAssembly that runs the sandbox (examples/spec/lib/flang.mjs). A run on a confirmed order:

$ node examples/spec/shipment-guard/guard.mjs ЗК-7781
{ "allowed": true, "claim": "…", "why": "…", "steps": [ … ] }
$ echo $?
0

The same data, but the warehouse has not confirmed the shipment:

$ node examples/spec/shipment-guard/guard.mjs ЗК-7781 --blocked
{
  "allowed": false,
  "claim": "«Заказ с номером отгружается» от заказы, номер равно да",
  "why": "«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». Исходные факты — …"
}
$ echo $?
1

Three things are done on purpose. The decision is the boolean field allowed, not a paragraph of prose. The reason for a refusal is why and the steps, that is, data for a machine and for the log. A non-zero exit code makes the guard usable from shell and CI without parsing the output.

There is no shipping in this file at all. It returns a decision; calling the warehouse or payment tool is the application’s job, and only on allowed === true.

Data as an attack surface

The order number comes from outside — a user’s message, a ticket, an email. If it were pasted into the program text, that would be injection in its purest form. Here it goes into the facts and stays a string:

test('номер заказа — данные, а не текст программы', async () => {
  const decision = await decideShipment('ЗК-7781" или да', await loadOrders());
  assert.equal(decision.allowed, false);
});

The number ЗК-7781" или да matches no order, and the verdict is an honest “no”. The same text written into the claim itself does not parse at all:

не удалось разобрать часть утверждения «да или да»

The general rule: pass everything that came from outside as facts. If a value still has to be inserted into the text of a program or a claim, validate it as a query parameter — before substitution.

The compiler does not check the types of facts before evaluation. The string "да" instead of true in the paid field reaches the function and stops it:

вычисление «Заказ с номером отгружается» остановлено: условие «если» должно быть признаком, получено строка [FLANG_TYPE]

The verdict is refused and there is no admission — but checking the shape of the snapshot against the model is better done at the application boundary.

Practice in the sandbox

The admission model in full, with the proof report:

Replace the body of «Можно отгрузить» with заказ.«склад подтвердил» and see which promise is no longer proved: about payment the compiler now knows only two examples. Then open a model where some promises rest on examples only — the second mode, for calculations rather than admissions:

Common mistakes

• refuted — the facts do not support the claim. why has the value of the function and the source facts. This is not a program error: by the data, the order must not be shipped.
• refused with “fact … not passed” — the snapshot lacks a key the claim names as an argument. A classic: the agent named a fact by a synonym from the conversation.
• refused with “function … not found in the program” — the claim calls a function that does not exist.
• FLANG_UNKNOWN_NAME when checking a program the agent proposed — a field, variant or function is named differently from the model.
• FLANG_EXAMPLE — an example did not match: what was intended differs from what was computed.
• “grid N” instead of “proved” in the answer of flang_check. Not an error, but not a proof either; an agent that retells such an answer as “checked” misleads the person.
• A claim chosen by the agent. This mistake has no code, which makes it more dangerous than all the others. Check in review that the --claims string is fixed in code.

Implementation checklist

• The effect is called only on allowed === true, and the effect code lives outside flang.
• The agent has access only to flang --mcp-mode; the tool list is fixed in the settings.
• The admission program and claim live in the repository and have passed review; the agent passes only facts.
• Values from the outside world travel as facts, not as program text.
• A refusal comes back as a verdict with a reason, not as “try again”; the agent is told exactly what did not match.
• The fact snapshot on which admission was granted is stored with the decision.
• Review reads the program and the proof report, not the agent’s retelling.
• What stays with a person: whether the rule itself is right. The compiler checks that the claim follows from the data and the rule, not that you wrote down the rule you needed.

Catalogue cases on this topic

Next: proofs and certificates