How Digit’s verifiability is structured

Hallucination is a situation where a language model generates factual tokens. It can be addressed in two ways: by persuading the model not to invent things or by removing the channel through which the generated content reaches the response. Digit is designed using the second approach.

The model generates only choices. The content is taken from three sources.

The difference between the two classes of fallacies is fundamental here. A selection fallacy yields a “wrong answer” or “could not find.” A generation fallacy yields an invented fact. The first class remains and can be measured. The second is closed off structurally.

Source one: a deterministic utility

Utilities are pure functions: hashes, encodings, format converters, address parsing, date handling. 95 utilities in 14 categories, migrated from 75 original browser tools out of 86. 11 were not migrated deliberately: they require a live browser, file loading, or are a cheat sheet rather than a calculation.

Each utility includes at least one working example; there are a total of 114 examples, and all of them are executed by a test suite, and then re-executed through the compiled binary using the same protocol as the agent. There are 220 tests.

A minor discrepancy, which is better to acknowledge than to gloss over: the training dataset for the router covers 94 utilities, while the catalog lists 95. The source of the difference is not explained in the reports.

Key to verifiability: the model does not write the result. It specifies the utility identifier and arguments, and then calculates the code. If there are not enough arguments, the call will not be made – instead of an answer, there will be a rejection indicating which argument is missing.

The entire catalog cannot fit into the context — the schemas of 95 utilities are too expensive for a small model. Therefore, routing is two-stage: first, the index of categories (≈536), then the schemas of utilities of one category. Three tools are exposed instead of 95 schemas.

Source two: a verbatim quote with an anchor

The second source is the course materials. The index is compiled from the corpus and contains 29,775 fragments; the search is hybrid — dense vectors from the intfloat/multilingual-e5-base model combined with lexical search, with a cross-encoder BAAI/bge-reranker-v2-m3 on top, which evaluates the “question + fragment” pair as a whole.

In this mode, the answer is not a paraphrase. It is a substring of a specific file plus an anchor to that file. The check is twofold: the fragment must be verbatim both in the index and in the current version of the corpus file. The second half of the check did not arise from theory: during one of the tasks, a neighboring process rewrote part of the corpus, the index remained old, and the system began to diligently quote the surviving neighboring fragments instead of the missing ones. Comparing with the file turned this into a rejection.

And it works right now, not only in history. The index was built on 3 August; as of 9 August, checking each of the 29,775 fragments against the file it was cut from gives 20,936 matches, 8,788 drifted offsets and 51 fragments from four files that no longer exist: in six days the corpus moved on by 29.5% of the fragments. What can be quoted today is 20,936 of 29,775 — for the rest the system must refuse, and it does. The number 29,775 is the size of the index, not a promise that all of it can be shown to a reader; what can be shown is what still matches the file.

Source three: a certificate over verified morphisms

A third source is needed where the answer is not a fact from the text or the result of a calculation, but a conclusion based on the rules of the subject area: “is a discount applicable,” “what rate is applied.” Such rules are written in FTS, a language for executable specifications, and the specification passes through a gate of several checks, each with its own failure code. There are a total of eight codes: syntax parsing, static semantics, validity of each premise, execution of author’s examples and declared properties, certificate generation, independent re-check, library integrity, and code for unforeseen conditions.

A separate layer is a detector of structural fallacies: eight codes, each of which is an algorithm applied to the parsed specification. A circle in the foundations, the application of implication in reverse, an uncovered branch of the walkthrough, a threshold without declared behavior exactly at the boundary, one name for a thing and for a statement about the thing. The catalog on which the detector is built contains 67 items; 12 are mechanically checked. The remaining 55 are rhetoric and content that cannot be resolved by an algorithm.

The premises are taken not from the specification text, but from a separate library: 29 entries, of which 18 have been verified by a human and contain a link to the source, 3 are derived through typed composition from the verified ones, 3 have the status “proposed” and cannot be premises. The gate has 62 tests, and the FTS library itself has 59.

The limit of the formal layer, explicitly named

FTS guarantees: if the premises are true, then the conclusion is true. The truth of the stated law is a premise, not a theorem. A specification that asserts a false domain axiom passes the check, tests, and certification completely green.

In the gateway documentation, this is presented as a working counterexample: the specification imposes a tax on the export supply at the standard rate instead of zero. The three teams of formalists perform flawlessly, the certificate is correct, and the fallacy detector does not find any of the 67 items in the catalog. The error is caught not by a mathematician, but by an entry in the library of morphisms, where a person entered the verdict “checked and rejected.”

Hence, an unpleasant but honest consequence: by eliminating structural defects, the detector makes the false conclusion smoother, not more accurate. The only point where the subject matter truth is decided is the review of the morphism when it is added to the library. The strength of the guarantee here is equal to the strength of the review, not the strength of the formalism.

Two modes and a ban on silent degradation

Mode A — verified. Content sourced only from the three sources listed above. Guarantee: zero fabricated facts. Price: a significant number of rejections.

Mode B — advisory. Free model generation. No guarantees, explicitly stated.

The main invariant of the entire structure: mode A does not silently degrade into B. If a request does not fit into A, then either it is rejected, or there is an explicit transition to B with a note. Replacing it with “I could not verify, but I will still answer” breaks the entire structure: the meaning of mode A is that the user does not need to guess whether a specific answer has been verified.

Therefore, a separate metric with a target value of zero has been established for mode leakage, and it is strictly measured: a response claimed to be mode A must provide at least one verifiable piece of evidence – a resolvable utility call, a valid quote, or a compilable specification. A response without evidence is counted as a leakage, even if it is correct in essence.

Before each answer is provided, an invariant check is performed: for each element of mode A, there must be a resolvable origin – the file exists and the text is present in it, the utility identifier is in the directory and the arguments are attached, and the certificate has a digest. In the final run, there are zero invariant violations.

Rejection accepts code, not a model

This is more important than it seems. When a regular assistant “doesn’t respond,” it’s a choice: it can be rephrased, persuaded, or worked around. Digit’s refusal in verifiable mode is the result of a deterministic check.

Three gates verify the origin, and each refusal carries its own name. The names are the ones that stand in the search code (rag/src/rag/retrieve.py), not ours:

Verbatimness is the fourth check and is built differently: verify_quote() answers yes or no to whether the answer text stands as a substring inside the fragment. It is not a refusal code but a condition without which the answer never leaves.

The order in the list is the order of firing, and it is not decorative. On 173 questions about what the corpus does not hold, the refusals fell out like this: 113 stopped by gate 0, 59 by the threshold, 1 by candidate disagreement (measured 2026-08-09, cross-encoder mode). Gate 0 stands first and takes two thirds — it, not the threshold, does the larger part of the work.

The fourth gate checks not the origin, but the relevance: whether the found fragment relates to the given question. It appeared after an independent set showed that most of the remaining fallacies were located there. The decision is also made by code here: none of the paths in this module asks the model whether the fragment answers the question. All the rules are string comparisons with word boundaries and a walkthrough of the superficial syntax of the query.

Two out of four implemented rules are working:

• Entities of the question. Latin tokens, identifiers, abbreviations, proper nouns, and literals in backticks are extracted from the query, and each must be found in the fragment at a word boundary. This rule eliminated 8 false answers.
• Circumstance instead of data. Before calling the utility, each argument is checked to see what it governs in the query itself. “Calculate the statistics of the text in windows-1251 encoding” does not contain text; it contains an indication of the encoding. The rule eliminated 4 false answers.

Two more rules were implemented, measured, and turned off because they did not eliminate a single false answer: a rule that doesn’t fix anything but can reject, is a pure risk on unseen data. All the rules together resulted in zero broken correct answers.

Separately, there is a certification gate. For a morphism that is not in the verified library, the corresponding function is not defined, the typing rule is not applicable, and there is simply no inference. The system did not “decide to remain silent”: it could not construct a proof. There is nothing to argue about here.

Rejection with numbers, instead of “I don’t know”

The wording of the rejection is structured as a statement about a closed domain and must include numbers. An example of the format (the numbers in it are illustrative – in a real rejection, the actual values of the run are used):

This is not present in the Digitable course materials. 12 fragments were checked, with a maximum relevance of 0.31, while the threshold is 0.55.

The strict reason is: “no answer” without specifying the search area and without numbers – this is, in itself, an unverifiable statement about the world, that is, the same hallucination, only more modestly dressed. Each refusal carries a code, a search area, and numbers: how many fragments were checked, which entities of the question were not found, which argument was missing.

The same principle applies in the opposite direction as well. A fallacy detector’s refusal is not an assertion of falsehood: the identified fallacy name returns the thesis to a “not shown” state, rather than refuting it. This is enforced by a test that mechanically prohibits the words “false” and “incorrect” from appearing in the refusal text.

The Role of a Small Model

In such an architecture, the model does not generate the answer but classifies the request and extracts the arguments. Therefore, it can be small – currently, it is Qwen/Qwen3-1.7B, selected based on performance metrics rather than its name.

The test, by the way, refuted the expectation. Russian-language instruct-tuning on top of the same base performed worse than the base itself on all key metrics: it improves dialogue, which we don’t use, and blurs some of the original capabilities. A model with an expanded Russian vocabulary provides real token savings and better routing, but it sacrifices the accuracy of argument extraction – and in the tested architecture, a utility called with an incorrect argument produces a verified incorrect answer, while an incorrectly selected utility most often fails the check and is visible.

We had to train it separately to refuse. In a typical training corpus, each question has an answer, so the model learns the meta-rule that “an answer always exists” and confidently invents an answer when there is no answer in the query. The solution is to increase the proportion of training examples where the correct answer is “refusal”: 23.8% of 34,709 lines. Conscious refusal during red-team testing increased to 91.3%, and the proportion of incorrect answers decreased to 9.2%.

And a fair disclaimer: the data did most of the work, not the model size. The same dataset with a three times smaller base yields a conscious rejection rate of 90.7% versus 91.3%.

All of this can be downloaded and re-checked.

The statements above can be verified not only in words. The models, training data, and task set are publicly available:

What each of these eight entries covers, what numbers confirm this, and what it cannot do can be found in the open models catalog. The same list is printed by the agent itself: digit model --catalog.

Along with the generator, a negative control is provided – 4,400 deliberately spoiled documents and the verdict of the verification gate for each. It is published as data, not as a table, so the stated “gate catches 91.6% of forgeries” can be recalculated by anyone from the same data, rather than being taken at face value.

The losers are published intentionally and on equal footing with the winners. A negative result, left in someone else’s drafts, turns into folklore: the next person who takes on the Russian-language base will spend the same weeks again— unless they see how it ended with us.

What follows from this

The structure provides exactly one thing: the content of the answer has a resolvable origin. It does not provide either the correctness of the source selection or the truthfulness of what is recorded in the corpus and in the library of morphisms.

What the measurements revealed and what it cost — on the next page. Where the boundary lies and what the system doesn’t detect — on the third page.