Исполняемые спецификации на flang AI-агенты и MCP: допуск выдаёт компилятор, а не текст модели
English
 0%

AI-агенты и MCP: допуск выдаёт компилятор, а не текст модели

9 мин 1846 слов
#flang#ai agents#mcp#digit#verification

AI-агенты и MCP: допуск выдаёт компилятор, а не текст модели

Языковая модель хорошо переводит обсуждение в черновик правила и хорошо объясняет результат словами. На роль последнего арбитра она не годится: ответ вероятностный, а убедительность текста никак не связана с его правильностью. Фраза «заказ готов к отгрузке, можно отгружать» — не допуск, а гипотеза. Допуском её делает отдельный шаг: вычисление утверждения на реальных данных, у которого два исхода и понятная причина при отказе.

Глава про то, как собрать такой шаг вокруг flang и где проходят границы ответственности между агентом, компилятором и приложением.

Минимальный пример

Правило и поиск заказа по номеру — полная программа, она проходит проверку и оба обещания доказаны:

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

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

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

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

Факты — обычный JSON-снимок данных, не часть программы:

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

Утверждение, которое решает допуск, — одна строка:

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

Что делает компилятор

Проверка идёт тремя независимыми шагами, и у каждого свой ответ.

flang check разбирает программу, проверяет типы и имена, доказывает завершение каждой функции и прогоняет примеры. Несуществующее поле, вариант или функция дают FLANG_UNKNOWN_NAME, несошедшийся пример — FLANG_EXAMPLE.

flang check --proof добавляет отчёт о доказательствах: какое обещание доказано для всех входов, какое проверено только на примерах («сетка N»), какое просто объявлено. Код возврата 0 — доказано всё, 3 — не всё.

flang facts вычисляет утверждение на фактах и отвечает JSON:

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

В steps — что взято из фактов, что функция вернула и с чем сравнили. Статус бывает трёх видов: verified — утверждение выполнено, refuted — вычислено и не выполнено, refused — вычислить не удалось (нет факта, нет функции, факт не того типа). Код возврата 1 при refuted и refused — это ответ «нельзя», а не сбой инструмента.

Вызывать flang facts можно только тотальные функции. Без пометки тотальная ответ звучит так:

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

Контур: предложение → проверка → допуск → эффект

  1. Агент предлагает правило — программу на flang — или собирает факты.
  2. Компилятор проверяет программу: типы, завершение, примеры, доказательства.
  3. Человек принимает правило в репозиторий, как любой код.
  4. В боевом пути приложение вычисляет фиксированное утверждение на фактах (flang facts) и получает «да» или «нет» с причиной.
  5. Приложение выполняет эффект — только по «да».

Эффект всегда снаружи. Функция flang не умеет отгрузить заказ, списать деньги или отправить письмо: действие в языке — это описанное значение, которое исполняет тот, кто запустил программу. Агент не может «случайно» отгрузить заказ через проверку, потому что у проверки нет такой способности в принципе. Максимум, чего он добьётся, — allowed: true там, где факты это подтверждают.

MCP-средства

flang --mcp-mode — служба для ИИ-помощника: JSON-RPC по стандартным потокам, по сообщению на строку. Прописывается в настройке помощника так:

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

Средств два:

Средство Аргументы Что отдаёт
flang_check source разбор, типы, завершение и отчёт о доказательствах целиком
flang_prove source, claim чем доказано одно названное обещание — или причину отказа

claim у flang_prove — имя обещания из строки обеспечивает «имя» ….

Главное свойство этих ответов: поля «ок» в них нет. Три вердикта — «доказано», «сетка N» и «объявлено, не доказано» — уходят порознь, и в начале каждого ответа стоит словарь этих слов. Ответ flang_prove на модели из главы 9 начинается так:

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

Программа, не прошедшая проверку, получает отдельный ответ: «Программа НЕ ПРОШЛА проверку языка, и ведомость доказательства поэтому не печатается» — и следом код ошибки. Признака ошибки на уровне протокола нет, поэтому клиент читает текст вердикта, а не только факт успешного вызова.

Чего в MCP-службе нет: вычисления на фактах. flang facts — команда двоичного, а не средство службы. Это правильно для контура: проверять правило агент может сам, а допуск по данным выносит приложение.

Служба не читает файлы и не ходит в сеть: программа приходит аргументом вызова. Это не защита от prompt injection, но это меньше поверхность: средство, которое агент зовёт чаще всего, физически не умеет ни читать диск, ни менять состояние.

Агент собирает факты, а не текст программы

Генерация программы текстом всегда оставляет шанс на ошибку: не та кавычка, забытый отступ, лишняя строка. Компилятор такую ошибку поймает, но в боевом пути её не должно быть вовсе. Поэтому роли делятся так:

  • программа и утверждение лежат в репозитории и прошли ревью;
  • агент выбирает, о чём спросить: номер заказа, снимок данных;
  • как спросить, решает код приложения.

Собрать программу на flang из JSON нельзя: flang ast переводит программу в JSON, но обратной дороги у компилятора нет. Значит, всё, что приходит от агента во время работы, должно приходить данными — фактами для flang facts.

Утверждение агенту тоже не отдают. Если бы агент выбирал строку --claims, он мог бы спросить «… равно нет» и получить честное verified — на заказе, который отгружать нельзя:

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

Компилятор здесь прав: утверждение действительно выполнено. Ошибка была бы в том, что приложение спросило не то.

Guard в коде

Рабочий пример лежит в репозитории курса: examples/spec/shipment-guard/guard.mjs. Утверждение — константа модуля, номер заказа и снимок данных уходят в факты:

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() берёт двоичный flang, если задана переменная FLANG_BIN, иначе — тот же компилятор в WebAssembly, на котором работает песочница (examples/spec/lib/flang.mjs). Запуск на подтверждённом заказе:

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

Те же данные, но склад отгрузку не подтвердил:

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

Три вещи сделаны намеренно. Решение — булево поле allowed, а не абзац прозы. Причина отказа — why и шаги steps, то есть данные для машины и для журнала. Ненулевой код возврата делает guard пригодным для shell и CI без разбора вывода.

Отгрузки в этом файле нет вообще. Он возвращает решение; вызвать складской или платёжный инструмент — работа приложения, и только по allowed === true.

Данные как поверхность атаки

Номер заказа приходит извне — из реплики пользователя, тикета, письма. Если бы он вклеивался в текст программы, это была бы инъекция в чистом виде. Здесь он уходит в факты и остаётся строкой:

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

Номер ЗК-7781" или да не совпадает ни с одним заказом, и вердикт — честное «нет». Тот же текст, вписанный в само утверждение, не разбирается вовсе:

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

Правило общее: всё, что пришло извне, передавайте фактами. Если значение всё-таки приходится вставлять в текст программы или утверждения, проверяйте его как параметр запроса — до подстановки.

Типы фактов компилятор до вычисления не сверяет. Строка "да" вместо true в поле «оплачен» доедет до функции и остановит её:

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

Вердикт при этом refused, допуска нет — но сверку формы снимка с моделью лучше делать на границе приложения.

Практика в песочнице

Модель допуска целиком, с отчётом о доказательствах:

Замените тело «Можно отгрузить» на заказ.«склад подтвердил» и посмотрите, какое обещание перестало быть доказанным: про оплату компилятор теперь знает только два примера. Затем откройте модель, где часть обещаний держится только на примерах, — это второй режим, для вычислений, а не для допусков:

Типичные ошибки

  • refuted — факты не подтверждают утверждение. В why — значение функции и исходные факты. Это не ошибка программы: по данным отгружать нельзя.
  • refused с «не передан факт …» — в снимке нет ключа, который утверждение называет аргументом. Классика: агент назвал факт синонимом из разговора.
  • refused с «функция … не найдена в программе» — утверждение зовёт функцию, которой нет.
  • FLANG_UNKNOWN_NAME при проверке предложенной агентом программы — поле, вариант или функция названы не так, как в модели.
  • FLANG_EXAMPLE — пример не сошёлся: задуманное разошлось с вычисленным.
  • «сетка N» вместо «доказано» в ответе flang_check. Это не ошибка, но и не доказательство; агент, пересказывающий такой ответ словом «проверено», вводит человека в заблуждение.
  • Утверждение, которое выбирает агент. Кода у этой ошибки нет, поэтому она опаснее всех перечисленных. Проверяйте на ревью, что строка --claims фиксирована в коде.

Чек-лист внедрения

  • Эффект вызывается только по allowed === true, и код эффекта лежит вне flang.
  • Агенту доступна только flang --mcp-mode; список средств фиксирован в настройке.
  • Программа и утверждение допуска лежат в репозитории и прошли ревью; агент передаёт только факты.
  • Значения из внешнего мира едут фактами, а не текстом программы.
  • Отказ возвращается вердиктом и причиной, а не фразой «попробуй ещё раз»; агенту сообщается, что именно не сошлось.
  • Снимок фактов, на котором выдан допуск, сохраняется вместе с решением.
  • На ревью читают программу и отчёт о доказательствах, а не пересказ агента.
  • Что остаётся человеку: правильность самого правила. Компилятор проверяет, что утверждение следует из данных и правила, но не то, что вы записали нужное правило.

Кейсы каталога по этой теме

Дальше: proofs и certificates

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Нужен разбор именно вашей ситуации?

Статья описывает общий случай. Если у вас частный — можно разобрать его отдельно, платно. А если не хватает целого материала, предложите тему: её оплачивают вскладчину, и она выходит открытой для всех.

Доска запросов
Дальше