Requirements checked before implementation: spec corpus, constitution, and ftspec

A new requirement is checked today by memory. Someone in the team remembers that the discount limit was capped at thirty percent at the board meeting in March, and notices that the fresh spec promises forty. If not remembered, the contradiction disappears into the implementation and surfaces in production when both code branches are already written and deployed.

The check can be made machine-based and run before the first line of code is written. The condition is exactly one: the requirements carrier is not markdown, but a compilable model. The tool is called ftspec and lives in github.com/digitable-lol/flang next to the project compiler ftsc and executor ftsvm. It has no parser of its own: parsing, module linking, and functor laws are handled by ftsc, model execution is performed by the FTS core.

Minimal example

Project Constitution — a standard FTS model. Its utilities play the role of invariants: they accept decision facts and return a violation count, zero means «everything is in order». Service field итог — the result of the spec utility being checked.

категория «Конституция»

  объект «Решение»
    сумма является деньгами
    итог является деньгами

  утилита «Предельная скидка»
    принимает «Решение»
    возвращает число
    начинает с 0

    правило «Скидка превышает тридцать процентов суммы»
      если итог больше 30 процентов от поля сумма
      то результат равен 1

    свойство «Нарушение считается один раз»
      результат не больше 1

    пример «Скидка в пределах»
      дано сумма равна 10000
      дано итог равен 2000
      ожидается результат равен 0

    пример «Скидка ровно на пределе»
      дано сумма равна 10000
      дано итог равен 3000
      ожидается результат равен 0

    пример «Скидка сверх предела»
      дано сумма равна 10000
      дано итог равен 4000
      ожидается результат равен 1

In the corpus file, another line модуль «Конституция» precedes the category — it is stripped by ftsc, and the core sees the category itself. Examples are mandatory here as well: an invariant that is not checked itself cannot be used to check others.

The requirement lives in a separate category and looks just as mundane:

    правило «Давнему подписчику сорок процентов»
      если «давний подписчик» равен да
      и сумма не меньше 500
      то результат равен 40 процентов от поля сумма

None of the lines here are marked as “controversial”. The conflict is found by ftspec check.

What the compiler does

1. ftsc parses corpus files, links modules by использует and экспортирует and checks the laws of functors. Errors from this layer come with codes FTSC_MODULE_* and FTSC_FUNCTOR_* and do not reach the requirements analysis stage: an unlinked corpus is meaningless to check.
2. The core executes examples of all models in the corpus — constitutions, specs, and memory. A model with a diverging example is not considered valid.
3. ftspec compares rule conditions from different specs, runs spec utilities against the constitution invariants, and calculates rule coverage by examples.
4. The result is JSON in stdout, diagnostics in stderr, and a nonzero return code on conflicts: the same contract as the core and ftsc check.

Corpus layout

constitution.fts                              инварианты проекта
memory/001-предел-скидки.fts                  принятые решения
specs/001-скидка-постоянному-клиенту/spec.fts одна фича — одна категория
mapping/скидки-в-подписки.fts                 функторы между категориями спек

A file’s role is defined by its place in the tree, not by its content: otherwise, it would have to be declared inside the file, and the declaration could be forgotten. The spec identifier is the name of its directory, so the feature is named the same in the report as in the tracker.

Four places answer four different questions. constitution.fts — what is always true and not discussed in a separate requirement. specs/ — what a specific feature requires; one feature — one category, because a category is the boundary within which object and field names mean something. memory/ — why the decision was made exactly this way: a decision recorded by a model with examples remains checkable three years later, while a decision recorded in a paragraph of correspondence does not. mapping/ — a dictionary between specs: objects of different categories are formally different types, and only a functor gives the right to consider “Order” from one spec and “Subscription” from another as one concept.

What is checked by the machine

Conflict of rules is resolvable by interval arithmetic

The FTS rule condition is a conjunction of comparisons of field with operand, there are exactly six operators. If the operand is a constant, the conjunction breaks down by fields: they are independent, so the intersection of two conditions is non-empty exactly when the intersection of constraints for each field is non-empty. A constraint on a single field is an interval with open or closed ends and a finite set of punctured points from не равен (number), a subset of {да, нет} (flag), or “everything except listed” (string and date). All three cases are solved exactly and in linear time: an SMT solver is not needed here, the task does not reach it. This is calculated without rounding in one’s favor — > 5 and ≥ 5 together give (5, +∞), not [5, +∞); ≥ 5 and ≤ 5 — exactly the point 5; ≠ 5 on [0, 10] punctures a point, and on [5, 5] makes the set empty.

Non-empty intersection by itself is not a conflict: rules can safely fire together. Conflict occurs when actions are incompatible. set to different values is a conflict. set versus add is a conflict because the outcome depends on the application order, and no order exists between specs. Along with the response, a witness is provided — a specific input where the requirements diverge:

FTSPEC_RULE_CONFLICT — правила «Постоянному клиенту десять процентов» и
«Давнему подписчику сорок процентов» (объект «Подписка») применимы одновременно
при «давний подписчик» = да, «сумма» ∈ [1000, +∞): оба правила задают
результат, но разными значениями
  пример входа: {"давний подписчик":true,"сумма":1000}

You don’t argue with a witness — you plug him into both models and watch. This is a different conversation from “I think there is a contradiction here.”

Constitution violation is checked on the input grid

The spec utility runs on a final grid derived from the thresholds of its own conditions: for a numeric field, all thresholds and their neighbors “threshold ± step” (the boundary не меньше 500 distinguishes 499, 500, and 501), for a flag — both values, for a string — constants from the conditions plus one external. At each point, the utility’s result is calculated, it is substituted into the итог input field of the invariant, and the invariant is executed by the kernel. A non-zero response — FTSPEC_CONSTITUTION, and the input is named in the diagnostics:

утилита «Скидка подписчику» нарушает инвариант «Предельная скидка» конституции
при «сумма» = 500, «давний подписчик» = да: результат 200, нарушений 1

The grid size is limited, truncation is deterministic: rerunning gives the same verdict. A point at which the utility itself rejects input by its свойством, drops out — it is not the checker’s job to argue with the model about its own admissions.

Coverage, duplicates, orphaned memory, functors

FTSPEC_UNCOVERED (warning) — the rule is not triggered by any example. Activation is defined by execution through the core: a probe utility is built from the rules 0..i, where the action of rule i is replaced with a label; previous rules remain untouched because the condition may refer to the accumulated result. An uncovered rule is not an error, but it is exactly what no one has checked.

FTSPEC_RULE_DUPLICATE (warning) — identical conditions and action in two specs. Not a conflict, but a request for a common module.

FTSPEC_MEMORY_STALE (error) — a solution in memory/ refers to a file or category that no longer exists. A reference to emptiness is worse than absence: it continues to be cited.

Functor laws — FTSC_FUNCTOR_* — come fully from ftsc check: totality, field types, morphism shape, composition preservation.

Honest boundary

This is not a proof of the consistency of the requirements. Four specific things are checked, and none is complete.

• Dependencies between fields outside constant comparisons. Condition если скидка больше 30 процентов от поля сумма links two fields, and coordinate-wise intersection stops working. Such pairs of rules are considered in summary.skippedPairs: they are not “checked and clean”, they are unchecked.
• Quantifiers and collections. “No client order should…” cannot be expressed in FTS — the language has no list type or recursion. Such requirements are not seen by the tool at all.
• External data. A rule depending on a reference, exchange rate or time cannot be checked: the model does not contain them.
• Violation strictly between grid nodes. The choice of points is empirical: rule behavior changes at condition boundaries. A violation living inside an interval and not reaching the edge will be missed. Reducing the step expands the grid, but does not ensure completeness.
• Synonyms not recorded by the functor. If two specs speak of one concept using different words and this is not declared anywhere, the conflict will not be found. Done intentionally: a guessed synonym causes a false alarm, and it is more expensive than a miss — after the third time the team stops reading the report.
• Two rules добавить are not considered a conflict. Addition is commutative, the result does not depend on the order. Absurdity of a total discount of 60 percent — a human judgment; the machine is told about it by recording the limit in the constitution, and only then will it start to be violated.

In other words, the tool answers the question “is there an input on which two requirements diverge,” and answers precisely where they are recorded by comparisons with constants. Everything else it honestly calls unverified.

Agent Role

Digit skills are located in github.com/digitable-lol/digit, in skills/software-development/, and are distributed by stages, not by tools. fts-constitution introduces project invariants. fts-specify transforms a customer requirement into a category with rules, properties, and examples. fts-admit runs ftspec admit <корпус> --spec specs/003-промокод and receives a verdict for one specification: the response contains only diagnostics in which itself participates. The corpus can live for years with known technical debt — this is not a reason to reject a new requirement if it breaks nothing. fts-memory writes the accepted decision into memory/ model with examples.

The key point here is the same as in the module on agents (https://courses.digitable.life/en/post/fts/10-ai-agents/): the decision is made not by the model’s response text, but by a deterministic check. The agent effectively translates the conversation with the customer into a draft specification and clearly explains in words why ftspec rejected it. It does not function as an arbiter: accepted: true and the return code are reproducible, while “it seems there are no contradictions” — is not.

What this is different from GitHub Spec Kit

Spec Kit solves the same task and arranges the same entities: constitution, specs per features, plan, tasks. The difference is in the carrier. There, the spec is markdown, and consistency is evaluated by the language model: the answer depends on the prompt wording, the model version, and what ends up in the context, and two runs on the same corpus may diverge. Here, the spec is compiled, the check is deterministic, the conflict witness is a specific input, not a paragraph of reasoning; the step is placed in CI and blocks the merge. From the same model ftsc prints code in eight languages, so the spec and implementation do not physically diverge.

The price is stated honestly: FTS is a small language. There are no collections, quantifiers, recursion, string operations, or calling utilities from utilities. Requirements that do not fit into it remain as text and are checked visually—as before. The choice is not between “everything is checked” and “nothing is checked,” but between “part is checked by the machine, and it is known which part” and “everything is checked by the memory of the person who was at the meeting.”

Practice in the sandbox

1. The “Big Purchase” rule is limited by the threshold of 10000. Write down the threshold and neighbors порог ± 1 — these are grid nodes where the constitution invariant would be checked for this utility.
2. In the “Regular Customer” rule, replace то добавить 5 процентов with то результат равен 5 процентов and run the examples. “Big Purchase of a regular customer” will stop converging: 3000 against 1000. Exactly for this reason set against add between two specs is considered a conflict — the outcome depends on which rule was applied first, and there is no order between specs.
3. Add a rule with a threshold higher than all values in the examples (если сумма больше 1000000). The model will remain green — this case is caught by FTSPEC_UNCOVERED, not by tests.

Common Fallacies

• FTSPEC_RULE_CONFLICT are closed by renaming rules. A name does not move the boundaries of the condition: the witness will remain the same input. They will stop diverging only the modified thresholds or actions.
• A spec without a functor and the surprise that a conflict is not found. Until mapping/ does not say that a “regular customer” of one category is a “long-time subscriber” of another, there is nothing to compare the rules with. Silence means “not checked,” not “clean.”
• A constitution invariant without examples. Such a utility is executed, but using it to check other specs is trusting an unverified judge.
• An empty constitution. If the limit is not recorded anywhere, there is nothing to violate, and FTSPEC_CONSTITUTION will not trigger on any corpus. The absence of diagnostics here is not a sign of health.
• ftspec check on pull request instead of ftspec admit. check breaks the build for old technical debt of the corpus and teaches the team to ignore the red step.
• summary.skippedPairs are not read. A non-zero value with a green verdict — is the most valuable line of the report.

Checklist

• The requirement is modeled with examples before the implementation branch is created.
• The constitution exists, its invariants return the number of violations, and their own examples converge.
• Each feature is a separate directory in specs/ and a separate category; the directory name matches the identifier in the tracker.
• Concepts named differently in two specs are connected by a functor in mapping/ — otherwise, conflicts between them are not searched.
• The accepted decision goes into memory/ model, not as a paragraph in correspondence.
• On a pull request, ftspec admit --spec <спека> is run, on master — ftspec check; both block on errors, not on warnings.
• skippedPairs, uncovered rules, and the number of grid nodes are read: these are the boundaries of the check, not service noise.
• A conflict witness is analyzed by a person: it shows that requirements diverge, but not which one is correct.

Cases in the catalog on this topic