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

Код в этой главе записан в прежней поверхности языка — со словами категория, объект, утилита. Сегодняшний компилятор её слова читает, но программой такой файл не считает: файл, где есть только утилиты, flang check отклоняет. Разбор задачи в главе верен; синтаксис переносится по таблице из главы «Старые модели».

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

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

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

Утверждение о конкретном заказе выглядит так — это полная модель, она компилируется:

категория «Исполнение заказа»

  объект Заказ
    номер является строкой
    клиент является строкой
    оплачен является признаком
    «склад подтвердил» является признаком
    «готов к отгрузке» является состоянием «Готов к отгрузке»

  морфизм «Готовый заказ можно отгрузить»
    если «Готов к отгрузке»
    то «Отгрузить заказ разрешено»

  теорема «Заказ ЗК-7781 можно отгрузить»
    дано Заказ имеет «готов к отгрузке» равное да
    в данных заказы найти где номер равен «ЗК-7781»
    по морфизму «Готовый заказ можно отгрузить»
    следовательно «Отгрузить заказ разрешено»

Строка в данных — самая важная. Она превращает рассуждение в проверяемое утверждение: движок обязан найти в переданном JSON путь заказы[номер="ЗК-7781"].готов к отгрузке и убедиться, что там true.

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

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

compile разбирает естественный синтаксис в каноническую JSON-модель. Здесь ловятся синтаксические ошибки (FTS_NATURAL_NAME и соседи) и ссылки на то, чего нет: несуществующее поле даёт FTS_UNKNOWN_FIELD, несуществующий морфизм — FTS_UNKNOWN_FUNCTOR.

validate проверяет документ семантически и возвращает { valid, document, diagnostics } — без исключений, списком.

prove строит вывод. Если контекст передан, проверяется путь свидетельства; если данные не сходятся, вывода не будет.

Важная деталь, которую легко проглядеть: prove без контекста на модели выше проходит успешно и возвращает символический вывод

Исполнение заказа.Заказ.Type — заказы[номер="ЗК-7781"].готов к отгрузке (Заказ ЗК-7781 можно отгрузить)

Это утверждение о форме рассуждения, а не о заказе ЗК-7781. Символический вывод никогда не должен служить основанием для действия — допуск выдаётся только prove (или certify/verify) с реальным контекстом.

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

1. Агент предлагает .fts — исходник или канонический документ.
2. Компилятор проверяет грамматику и имена.
3. Для утилит исполняются примеры: расхождение реализации и ожидания видно сразу.
4. prove (строго — certify + verify) решает по данным.
5. Приложение выполняет эффект.

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

MCP-инструменты

Сервер (src/mcp.ts) говорит по stdio, реализует ревизию MCP 2025-06-18 и представляется как { name: "fts", title: "Formal Type Surface", version: "0.3.0" }. Десять инструментов, все помечены readOnlyHint: true, destructiveHint: false, idempotentHint: true, openWorldHint: false.

source и document заданы как oneOf с additionalProperties: false: передать надо ровно одно. input у fts_execute — объект скаляров (string/number/boolean/null), не произвольный JSON.

Почему read-only важно. Сервер не принимает путь к файлу: исходник и контекст приходят аргументами вызова. Модель не может попросить прочитать .env или чужую модель — такой параметр просто не существует в схеме. Это не защита от prompt injection (её здесь нет), но это сокращение поверхности: инструмент, который агент вызывает чаще всего, физически не умеет ни читать диск, ни менять состояние, ни ходить в сеть.

Отдельно: fts_certify и fts_verify используют node:crypto и живут только на серверной стороне. В браузерной сборке их нет — песочница на сайте компилирует, исполняет и доказывает, но сертификаты не выдаёт и не проверяет.

Агент строит документ, а не текст

Генерация исходника текстом всегда оставляет шанс на невалидный результат: не та кавычка, забытый отступ, лишняя строка. Есть путь надёжнее — собрать канонический документ программно. witnessDocument строит утверждение «поле такого-то объекта в данных равно такому-то значению»:

import { prove, witnessDocument } from '../../../static/js/vendor/fts/browser.js'

const document = witnessDocument({
  category: "Исполнение заказа",
  structures: [{
    name: "Заказ",
    fields: [
      { name: "номер", type: "string" },
      { name: "готов к отгрузке", type: "boolean" },
    ],
  }],
  structure: "Заказ",
  field: "готов к отгрузке",
  value: true,
  path: ["заказы", { номер: orderNumber }, "готов к отгрузке"],
  detail: `Заказ ${orderNumber} можно отгрузить`,
})

Результат — { category, structures, functors, proposition, ts_compat } с proposition.kind === "witness". Парсер не участвует, поэтому синтаксически невалидным этот документ сделать нельзя. Семантически — можно: если сослаться на поле, которого нет в structures, validate вернёт FTS_UNKNOWN_FIELD по пути $.proposition.field, а неизвестный объект — FTS_UNKNOWN_STRUCTURE по пути $.proposition.structure. Ошибка остаётся, но становится структурной и адресуемой, а не «где-то в тексте».

composeDocument делает то же для цепочки морфизмов: принимает category, structures, functors, chain (имена морфизмов) и arg — вложенное утверждение, и собирает proposition вида { kind: "compose", functors, arg }.

Практический вывод: пусть модель выбирает что утверждать (какой объект, какое поле, какой путь в данных), а как это записать — пусть делает код.

Guard в коде

Рабочий пример лежит в репозитории курса: examples/spec/shipment-guard/guard.mjs. Он строит теорему по номеру заказа, доказывает её на реальном снимке данных и возвращает решение:

export function decideShipment(orderNumber, context) {
  const source = shipmentTheorem(orderNumber)
  try {
    const proof = prove(compile(source), context)
    return { allowed: true, source, proof }
  } catch (error) {
    return { allowed: false, source, reason: error.message, diagnostics: error?.diagnostics ?? [] }
  }
}

Запуск на подтверждённом заказе:

$ node examples/spec/shipment-guard/guard.mjs ЗК-7781
{ "allowed": true, "source": "...", "proof": { ... } }
$ echo $?
0

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

$ node examples/spec/shipment-guard/guard.mjs ЗК-7781 --blocked
{
  "allowed": false,
  "reason": "witness does not match context at заказы[номер=\"ЗК-7781\"].готов к отгрузке: expected true, got false",
  "diagnostics": [
    { "code": "FTS_WITNESS_MISMATCH", "message": "...", "severity": "error", "path": "$.proposition" }
  ]
}
$ echo $?
1

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

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

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

Номер заказа приходит извне — из реплики пользователя, из тикета, из письма. Он подставляется в текст теоремы, а значит, это инъекция в чистом виде: закрыв кавычку-ёлочку и добавив перевод строки, можно дописать в модель произвольные конструкции. Поэтому в guard.mjs подстановке предшествует проверка:

const ORDER_NUMBER = /^[\p{L}\p{N}-]{1,32}$/u

export function shipmentTheorem(orderNumber) {
  if (!ORDER_NUMBER.test(orderNumber)) throw new Error(`недопустимый номер заказа: ${orderNumber}`)
  return `категория «Исполнение заказа» ...`
}

Регулярка допускает только буквы, цифры и дефис — символов, значимых для грамматики FTS, в этом классе нет. Тест фиксирует поведение:

test('номер заказа не может протащить произвольный текст в теорему', () => {
  assert.throws(() => shipmentTheorem('ЗК-7781»\n  теорема «взлом'), /недопустимый номер заказа/)
})

Правило общее: любое значение, попадающее в исходник конкатенацией, — параметр запроса, и валидировать его надо как параметр запроса, до подстановки.

Сборка через witnessDocument снимает проблему структурно: там номер оказывается значением селектора внутри JSON, а не фрагментом синтаксиса. Строка »\n теорема «взлом в роли номера даёт валидный документ и честный отказ FTS_WITNESS_MISMATCH — «записи с таким номером в данных нет», потому что текстом она так и не стала.

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

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

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

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

FTS_WITNESS_MISMATCH — данные не подтверждают утверждение. Сообщение содержит путь и оба значения: expected true, got false, а для отсутствующей записи — expected true, got <missing>. Строка "да" вместо true тоже даёт mismatch: типы не приводятся молча.

FTS_UNKNOWN_FIELD — агент назвал поле, которого нет в объекте: «не найдено поле «Заказ».«скомплектован»». Классический случай, когда модель подставила синоним из разговора вместо термина модели.

FTS_UNKNOWN_FUNCTOR — теорема ссылается на несуществующий морфизм.

FTS_PROOF_TYPE_MISMATCH — морфизм ждёт состояние, а поле объявлено признаком: «морфизм «Готовый заказ можно отгрузить» ожидает «Готов к отгрузке», получено «Признак»». Типичная правка агента, которая «упрощает» модель и ломает вывод.

Расхождение примера — fts_test возвращает valid: false и по каждому примеру expected и actual. Это не диагностика компилятора, а несовпадение задуманного с вычисленным.

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

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

• Эффект вызывается только по булеву результату проверки, и код эффекта лежит вне FTS.
• Агенту доступны только read-only инструменты; список фиксирован в конфигурации.
• Каждый допуск доказывается с контекстом; символический вывод в этот путь не попадает.
• Значения из внешнего мира валидируются до подстановки в исходник — или документ собирается через witnessDocument/composeDocument.
• Отказ возвращается кодом диагностики и путём, а не фразой «попробуй ещё раз»; агенту сообщается, что именно не сошлось.
• Снимок данных, на котором выдан допуск, сохраняется вместе с решением.
• На ревью читают исходник и диагностики, а не пересказ агента.
• Что осталось человеку: правильность самой модели. Движок проверяет, что утверждение следует из данных, но не то, что вы описали нужное правило.

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

Дальше: proofs и certificates