FTS for AI agents and MCP: the engine grants access, not the model text

A language model translates the discussion into a specification draft well and explains the result in words well. It is poorly suited for the role of the final arbiter: the answer is probabilistic, and the persuasiveness of the text has no connection to its correctness. The phrase “the order is ready for shipment, it can be shipped” is not a permit, but a hypothesis. A permit becomes it through a separate step: a deterministic check of the assertion against real data, which has exactly two outcomes and a stable diagnostic code on failure.

This module is about how to build such a step around FTS and where the boundaries of responsibility between the agent, the engine, and the application lie.

Minimal example

A statement about a specific order looks like this — it is a complete model, it compiles:

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

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

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

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

Line в данных — is the most important. It turns reasoning into a verifiable assertion: the engine must find in the provided JSON the path заказы[номер="ЗК-7781"].готов к отгрузке and ensure that true is there.

What the compiler does

The check proceeds in three independent stages.

compile parses natural syntax into the canonical JSON model. Here syntax errors (FTS_NATURAL_NAME and neighbors) and references to non-existent entities are caught: a non-existent field gives FTS_UNKNOWN_FIELD, a non-existent morphism gives FTS_UNKNOWN_FUNCTOR.

validate checks the document semantically and returns { valid, document, diagnostics } — as a list, without exceptions.

prove builds the inference. If the context is passed, the proof path is checked; if the data does not match, there will be no inference.

An important detail that is easy to overlook: prove without context on the models above passes successfully and returns symbolic output

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

This is a statement about the form of reasoning, not about order ZK-7781. Symbolic inference must never serve as a basis for action — access is granted only prove (or certify/verify) with a real context.

Kontur: offer → check → admission → effect

1. The agent offers .fts — source code or canonical document.
2. The compiler checks grammar and names.
3. For utilities, examples are executed: a discrepancy between implementation and expectation is visible immediately.
4. prove (strictly — certify + verify) decides based on data.
5. The application performs the effect.

The effect is always external. There is no shipping, no money deductions, no sending emails in FTS — the language can do nothing except computation and verification. This is not a limitation, but the design of the system: an agent cannot “accidentally” ship an order, because the verification code simply does not have that capability in principle. At most, it can achieve allowed: true where the data confirms it.

MCP-tools

The server (src/mcp.ts) communicates via stdio, implements MCP revision 2025-06-18 and is represented as { name: "fts", title: "Formal Type Surface", version: "0.3.0" }. Ten tools, all marked readOnlyHint: true, destructiveHint: false, idempotentHint: true, openWorldHint: false.

source and document are defined as oneOf with additionalProperties: false: exactly one must be passed. input at fts_execute — scalar object (string/number/boolean/null), not arbitrary JSON.

Why read-only is important. The server does not accept a path to a file: the source and context come as arguments of the call. The model cannot request to read .env or another model — such a parameter simply does not exist in the schema. This is not protection against prompt injection (there is none here), but it reduces the attack surface: the tool that the agent calls most often physically cannot read the disk, change the state, or access the network.

Separately: fts_certify and fts_verify use node:crypto and exist only on the server side. They are absent in the browser build — the sandbox on the site compiles, executes, and proves, but does not issue or verify certificates.

Agent builds a document, not text

Text-based source generation always leaves a chance for an invalid result: a wrong quotation mark, a forgotten indentation, an extra line. There is a more reliable way — to build the canonical document programmatically. witnessDocument constructs the assertion “the field of such-and-such object in the data equals such-and-such value”:

import { prove, witnessDocument } from "@digitable-lol/fts"

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

Result — { category, structures, functors, proposition, ts_compat } with proposition.kind === "witness". The parser is not involved, so it is impossible to make this document syntactically invalid. Semantically — it is possible: if you reference a field that does not exist in structures, validate will return FTS_UNKNOWN_FIELD along the path $.proposition.field, and an unknown object — FTS_UNKNOWN_STRUCTURE along the path $.proposition.structure. The error remains, but becomes structural and addressable, rather than “somewhere in the text”.

composeDocument does the same for the morphism chain: takes category, structures, functors, chain (morphism names) and arg — nested assertion, and builds proposition of the form { kind: "compose", functors, arg }.

Practical takeaway: let the model choose what to assert (which object, which field, which path in the data), and how to write it — let the code do that.

Guard in code

A working example is in the course repository: examples/fts/shipment-guard/guard.mjs. It builds a theorem by order number, proves it on a real data snapshot, and returns the solution:

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 ?? [] }
  }
}

Order confirmation launch:

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

Same data, but the warehouse did not confirm the shipment:

$ node examples/fts/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

Three things here are done intentionally. The resolution is a boolean field allowed, not a paragraph of prose. The reason for rejection is the code FTS_WITNESS_MISMATCH and the path $.proposition, that is, data for the machine. A non-zero return code makes the guard suitable for the shell and CI without parsing the output.

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

Data as an attack surface

The order number comes from outside — from the user’s replica, from a ticket, from a letter. It is substituted into the theorem text, which means it is a pure injection: by closing the quote and adding a line break, arbitrary constructions can be appended to the model. Therefore, in guard.mjs substitution is preceded by a check:

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

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

The regex allows only letters, digits, and hyphens — there are no characters significant for the FTS grammar in this class. The test captures the behavior:

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

General rule: any value that ends up in the source code by concatenation is a query parameter and must be validated as a query parameter before substitution.

Build through witnessDocument removes the issue structurally: there the number turns out to be a selector value inside JSON, and not a syntax fragment. String »\n теорема «взлом in the role of a number gives a valid document and an honest refusal FTS_WITNESS_MISMATCH — «there are no records with such a number in the data», because it never became text.

Practice in the sandbox

Model of the entire permission, with proof derivation:

Check what happens without data, and compare it with the section “What the compiler does”. Then look at the utility with examples — this is the second mode of checking, for computations rather than for permissions:

Common Fallacies

FTS_WITNESS_MISMATCH — data does not support the claim. The message contains the path and both values: expected true, got false, and for the missing entry — expected true, got <missing>. Line "да" instead of true also gives a mismatch: types are not silently coerced.

FTS_UNKNOWN_FIELD — agent mentioned a field that does not exist in the object: “field ‘Заказ’.‘скомплектован’ not found”. A classic case when the model substituted a synonym from the conversation instead of the model’s term.

FTS_UNKNOWN_FUNCTOR — the theorem refers to a non-existent morphism.

FTS_PROOF_TYPE_MISMATCH — the morphism expects a state, but the field is declared as a flag: «the morphism «A ready order can be shipped» expects «Ready for shipping», received «Flag». A typical agent edit that «simplifies» the model and breaks inference.

Example discrepancy — fts_test returns valid: false and for each example expected and actual. This is not a compiler diagnostic, but a mismatch between the intended and computed.

Symbolic inference, taken as a pass, has no code at all — and therefore is more dangerous than all listed. Check during review that context is passed along the production path.

Implementation checklist

• The effect is triggered only by a boolean result of the check, and the effect code lies outside FTS.
• The agent has access only to read-only tools; the list is fixed in the configuration.
• Each access is proven with context; symbolic inference does not fall into this path.
• Values from the external world are validated before substitution into the source — or the document is assembled through witnessDocument/composeDocument.
• Rejection is returned by a diagnostic code and path, not by the phrase “try again”; the agent is informed exactly what did not match.
• The data snapshot on which access was granted is saved together with the decision.
• During review, the source and diagnostics are read, not the agent’s retelling.
• What remains for a person: the correctness of the model itself. The engine checks that the assertion follows from the data, not that you described the required rule.

Cases in the catalog on this topic

Next: proofs and certificates