In a minute
A conversation on the subject of this page starts with a message to the scientific director of the institute.
Write to the scientific directorThe doctrine states the institute’s position: autonomous computing systems are taking over the functions of managerial and supervisory institutions faster than law and engineering can frame them, and the transition can be governed but not stopped. Two speeds meet in it: a collegial body decides over weeks, an autonomous system within milliseconds, and a direct meeting destroys both. The institute proposes an intermediary: a person signs the rule, a solver proves the admissibility of every irreversible action before execution, and the decision is recorded so that an outsider can check it. The institute is built by the same design: MITR (the institute’s proven-action system) has checked the actions of its own agents since 24 April 2026, and the discipline of decision records applies to the institute itself. The page is addressed to the owners of critical information infrastructure, to institutional capital and to research bodies, and it ends with the way to reach the scientific director.
The world is moving into a state that the established institutional forms cannot accept without rebuilding themselves. Autonomous computing systems have begun to perform functions that historically belonged to managerial, supervisory and intellectual institutions, and this is happening faster than the institutional environment can produce a legal and technical framework for it.
It follows that the transition is neither a voluntary choice nor a matter for debate: it takes place regardless of whether the institutional environment is ready to accept it. The question the institute answers is a different one: how this transition can be given a governable form.
Diagnosis: two incompatible speeds
The old world works on the time scale set by the procedure of collective decision. A board of directors, an academic council, a risk committee and an interagency approval process were devised to preserve the quality of a decision by slowing its adoption. That slowness is not a defect but a structural feature of the institutional form.
The new world works on the time scale set by an autonomous computing system, and a decision is made within an interval in which a collegial body cannot even convene. That speed is not a defect either: it is built into the very design of an autonomous system.
A direct meeting of the two speeds destroys both. An institution that tries to work at the pace of an autonomous system loses its institutional form, and an autonomous system forced into the institutional pace loses its functional value. An adapter must therefore stand between them.
Method: system synthesis
The method is set out in full on the page “The method of system synthesis” (in Russian).
The institute does not offer a choice between the old world and the new, because time has already made that choice. It offers a design in which both speeds keep their functional nature without destroying each other.
This is system synthesis, and it is not reducible to a hybrid or to a compromise between the two. Synthesis means that two incompatible elements are joined in a third form in which both are preserved in full but act through an intermediary that reconciles their regimes.
The intermediary is the institute itself. From the old world it takes the institutional requirements: the legal framework, the confidentiality regime, the approval procedure and regulatory compliance. From the new world it takes autonomous computing systems and brings them into a form compatible with those requirements.
In that construction institutional capital gains access to the new capacity without losing its own form, and the new capacity gains a form compatible with the requirements of that capital.
What is set out here is one application of the method: the separation of two incompatible speeds across different levels of governance. The method itself, its procedure, its conditions of failure and its limits are described separately, on the page “The method of system synthesis” (in Russian).
Principle: compliance by design
The common approach to integrating autonomous systems into an institutional environment adds compliance after the fact: the technology is deployed first, and regulatory wrappers, security policies and audit procedures are attached to it afterwards. The institute holds that this order is wrong in principle.
Compliance by design means that conformity with institutional requirements is built into the system at the level of its axioms, before the first line of code is written. Regulatory norms, corporate policies and risk limits are formalized as a set of axioms, and an action that has passed through MITR cannot contradict them: a deviation is blocked before any attempt at execution. The property that nothing passes around the check is secured by an installation in which MITR holds the keys to the target systems and the executor keeps only the right to request a check.
This impossibility of deviation refers to conformity with the formalized axioms: MITR guarantees that a permitted action does not violate the policy that has been translated into axioms. The correctness of that translation of a norm into axioms remains the responsibility of an authorized specialist, and MITR makes that specialist’s decision verifiable while leaving the last word with the specialist.
Compliance ceases to be a question of behavioral reliability, which probabilistic systems do not have and cannot have, and becomes a question of design in which deviation is impossible. It no longer depends on how well a model has been trained; it depends on the correctness of a proof.
compliance by design · axiomatic modeling of policies · Federal Law No. 187-FZ “On the Security of Critical Information Infrastructure of the Russian Federation” · Order No. 117 of the Federal Service for Technical and Export Control of Russia · GOST R 56939-2024 · GOST R 57580
Method: formal verification of decisions
How MITR checks an action step by step, with an example of a rule and the boundary of the guarantee, is shown on the page “How MITR works” (in Russian).
The core of MITR contains solvers for satisfiability modulo theories (SMT), the instruments that have long been used to check critical computing systems, including access rights in cloud infrastructure of global scale. Amazon’s Zelkova service performs on the order of a billion such checks a day, as Neha Rungta reported in the talk “A Billion SMT Queries a Day” at the Computer Aided Verification (CAV) conference in 2022. Every irreversible action of an autonomous executor is translated into a strictly typed predicate and is checked mathematically against the given axioms before execution.
Each such decision is therefore computable rather than probabilistic: it is either derivable from the axioms, in which case the action is admitted, or not derivable, in which case the action never reaches the point of execution. A probabilistic model can in principle be talked around its behavioral constraints; an axiomatic constraint cannot be talked around, because what is checked is the action itself. The attack set of 24 October 2026 names three known gaps in the rules of MITR, and closing them is in the plan of work.
The boundary of the guarantee is stated plainly. MITR provides soundness: a permitted action is guaranteed not to violate the formalized policy. The completeness and correctness of the translation of a norm or an intention into axioms belong to semantics and remain the responsibility of an authorized specialist.
MITR does not claim to be a silver bullet. It moves the point of control from unpredictable execution to a verifiable stage of translation, and it gives the person who makes the decision an instrument of verification instead of replacing that person. Grammar-constrained generation (constrained decoding) secures only the syntactic correctness of a specification; protection against semantic drift is achieved by translating the formal structure back into natural language so that a specialist can audit it before the check.
The novelty lies in applying formal verification, long known as an instrument, to the governance of autonomous systems as a normative environment: before the action is executed, and asynchronously.
The technological sovereignty of the core is arranged as follows. On the research bench the check is performed by the industrial solver Z3 (developed by Microsoft Research) as the reference for the method. The target result of the program is the institute’s own trusted micro-prover: a compact implementation of the decision procedure for the decidable theory of quantifier-free linear integer arithmetic with uninterpreted functions (QF_UFLIA), developed in a trusted environment.
The theory QF_UFLIA is decidable, so a check always terminates. At the same time the satisfiability problem in it belongs to the class of problems whose solutions are verified in polynomial time (NP) and is NP-complete: there is no guarantee of polynomial time, and in the worst case the growth is exponential. On the isolated, strictly typed predicates that arise in practice, the solver’s heuristics contain that growth, and a check takes milliseconds. The compactness of the institute’s own prover will make its deductive verification possible with the instruments of the Ivannikov Institute for System Programming of the Russian Academy of Sciences: the AstraVer platform built on Frama-C and Why3, with specifications in a formal specification language for C programs (ACSL). This is the route to evaluation by the assurance levels established by Order No. 76 of the Federal Service for Technical and Export Control of Russia (FSTEC of Russia) and to secure software development under the Russian national standard (GOST R 56939-2024).
The method is deployed in several independent layers of action checking. The irreversibility gradient classifies actions by the damage an error can cause, with reading without consequences (R0) at one end and irreversible destruction (R5) at the other. Declarative contracts are stored as data; since 24 October 2026 all 20 of them have run in enforce mode, and the decision is made by the solver without a call to a language model. The formal check of policy for irreversible actions goes through an SMT solver: on the bench the Z3 solver answers in 1.08 milliseconds at the median. The program of work provides for the institute’s own compact solver for the same logic, and a separate layer keeps the provenance of every fact on which a decision relies.
The protocols of transition between layers and the states of safe failure are to be specified and model-checked in TLA+, a language based on the temporal logic of actions (TLA). The deep correctness of the decision procedure and of code generation is to be proved interactively in Rocq, formerly known as Coq. As of 26 October 2026 both are plans of the program. The construction itself has been shown at work in the institute’s production system, and the deployment of the layers and their current coverage are described on the page MITR.
SMT · QF_UFLIA · sovereign micro-prover · AstraVer (assurance levels) · TLA+ · soundness
Operating form: an organization with agent execution
The institute is arranged so that its own structure coincides with its subject of research. The substantive part of the work, that is, the setting of tasks, the design decisions and the checking of results, is held at a single point of responsibility, while an autonomous corps carries out development, documentation, monitoring and maintenance. All working exchange is closed inside the institute’s own protected network.
This operating model was chosen deliberately: it shows at work what is offered to the customer. The institute does not describe an organization with agent execution from the outside; it has worked inside one from the first day of its founding and presents its working bench as direct evidence that the method applies.
In practice, the productive capacity historically attainable by a small research group is sustained by a design in which human responsibility stays in one node and the executive functions are distributed among deterministic executors under institutional policy. This proportion reflects the current point of the research program and is revised together with it.
The method demonstrated in production
The principles of the doctrine do not remain a declaration: the institute keeps them on display in a working MITR, the reference implementation, which has run continuously since 24 April 2026.
MITR serves the operator’s fiduciary tasks inside a closed perimeter. Every irreversible action passes through the layered protection described above: classification by degree of irreversibility, a deterministic formal check by the Z3 solver against 20 declarative contracts in enforce mode, and the provenance of every fact. The decision log satisfies the requirement to record security events in subparagraph “в” of paragraph 63 of the Requirements approved by FSTEC of Russia Order No. 117. That order has been in force since 1 March 2026 in place of Order No. 17.
MITR is at once the subject of the transaction and the research bench: the operating environment in which the institute checks invariants, formalizes policy and measures behavior under prolonged operation. The production regime gives the program methodological credibility: its statements about MITR are confirmed by the verifiable metrics of a running system.
The design of MITR, the roadmap of its extension, the format of the decision log and the model of openness are described on the page MITR.
Points of reference
The program rests on four lines: the cybernetics of control of William Ross Ashby and Stafford Beer, the theory of inventive problem solving of Genrich Altshuller, formal verification methods built on SMT solvers, and the Russian school of automata theory and mathematical economics. That school answered the questions that now stand before the institute: how to build a deterministic system in a nondeterministic world, how to keep control at scale, and how to translate thought into a form fit for computation.
Andrey Kolmogorov laid the foundations of probability theory and of algorithmic complexity. Victor Glushkov created automata theory and led the project of the nationwide automated system for information accounting and processing (OGAS), the first attempt in the world at a nationwide cybernetic system of government. Leonid Kantorovich developed linear programming and mathematical economics and received the Nobel Prize in 1975. Alexey Lyapunov founded Soviet cybernetics, and Norbert Wiener described cybernetics as the science of communication, control and feedback.
From each line a specific procedure or constraint has been taken; what exactly was taken and what was deliberately left aside is listed on the page “The method of system synthesis” (in Russian).
Whom the institute addresses
The institute works with three categories of institutional counterparties, and it has a distinct role with each.
The first category brings together the owners of critical information infrastructure and the holders of regulated processes: the banking and financial sector, the facilities covered by Federal Law No. 187-FZ of July 26, 2017, “On the Security of Critical Information Infrastructure of the Russian Federation”, and state information systems. Here the institute acts as the developer and integrator of formally verifiable autonomous systems able to pass regulatory review before deployment.
The second category is institutional capital that regards autonomous computing systems as a class of intangible assets in need of its own technical and legal form; here the institute acts as a methodological partner and co-architect.
The third category comprises academic and sectoral research bodies. The institute is open to joint research programs, expert councils and participation in dissertation work in its fields; inquiries are accepted through the Contact page with the subject “Research cooperation”.
Discipline of design decisions
The doctrinal principles of the institute do not remain declarations, and carrying them into production work requires an operating discipline that keeps the declared method and the actual practice in agreement. That discipline is fixed in the methodology of adopting and recording architecture decision records (ADR), a recognized engineering standard. The institute applies it recursively: both in the development of MITR and in the management of its own operations.
Purpose of the discipline
In work with autonomous computing systems the discipline of design decisions cannot be optional. Every decision made without a record and a rationale, in an environment where execution is delegated to an autonomous corps, creates an area of invisible responsibility: a state in which the system acts for reasons that the person in the chain of control can no longer reconstruct.
In conventional software development this problem is softened by the fact that code is written by people whose memory holds the context of a decision. In work with autonomous executors that context does not exist. A decision not recorded at the moment it is made disappears, and six months later none of the participants will be able to restore it.
Hence the requirement: every significant design decision is recorded as an ADR before it becomes part of the production system. This measure belongs to the very structure of work with a system in which memory is distributed between a person and an autonomous corps, while responsibility stays only in the human node.
Append-only records
The institute’s ADR are kept in append-only mode: a decision made at moment A with rationale B is not edited at moment C. If at moment C the decision is found to be wrong, a new ADR cancels it, with a reference to the previous one and the status “superseded by the ADR with the stated number”. Both records stay in the register, so the chain of decisions can always be reconstructed.
This requirement grew out of practice: the autonomous corps treats design decisions as input data. A retroactive change to an ADR on which an autonomous module has based its further decisions creates cascading uncertainty, a state in which no component of the system can rely on a stable foundation.
Append-only mode turns the ADR register into an uneditable log, analogous to the log of security events required by subparagraph “в” of paragraph 63 of the Requirements approved by FSTEC of Russia Order No. 117. Any reviewer, whether internal, external, academic or regulatory, can walk through the history of decisions in chronological order and reconstruct why the system is built the way it is.
The protected zone
Among the parts of the institute’s structure there is a protected zone: a set of files and modules that the autonomous corps does not change under any circumstances. It includes the code that measures quality metrics, the checks of the quality control component, the mechanism of research cycles, the register of active hypotheses and the source contracts under which the agents work.
An attempt by an autonomous module to change the protected zone is blocked before execution and recorded in the log of violations. The prohibition is set by file system access rights and by version control, so no instruction lets a module get around it.
The protected zone exists so that the measuring apparatus by which the institute evaluates its own work cannot be altered by those who perform that work. In financial reporting the same discipline is provided by the auditor’s independence from the audited entity; in an environment with many agents that independence must be built into the design.
Without a protected zone any autonomous module is in theory able to adjust the metric of its own success. With it there is no such possibility, and this rests on a technical impossibility that does not depend on the module’s promises.
The principle of one active experiment
The institute treats hypotheses as structured research units. Each hypothesis has a status (queued, active, closed as accepted or closed as rejected) and is tied to one asset that may change.
The principle of one active experiment means that at any moment only one component of the structure may change, and it is tied to one active hypothesis. Parallel changes are forbidden by the requirement of scientific method: with two simultaneous changes it is impossible to establish which of them caused the observed change in a metric.
This requirement puts the institute’s engineering work in a regime analogous to experimental science. Every change to the structure comes with a baseline of indicators, observation over a fixed period and an assessment of the difference by an objective metric, and only after that cycle is the change accepted or reverted.
Combined with append-only mode for ADR, this yields a traceable history of the institute’s experimental program: which hypotheses were tested, in what order, with what results, and which design decisions were adopted on their basis.
Budget discipline
Every autonomous module of the institute works within a formalized budget: computation per iteration, the number of iterations per week and an upper bound on cost. These limits are conditions that are checked before execution begins.
Budget discipline serves three functions. The first is financial: at any moment it can be established how much computing each module has spent, on which task and with what result. The second is operational: a module that has exhausted its budget for the current period stops until the next cycle begins. The third is ordering: the budget sets the priority of tasks, so a person does not have to rank them by hand.
The budget of each module is fixed in a register and changes only through an ADR with a rationale. Arbitrary extension of a limit is forbidden even to a module with administrator rights, because the protected zone requires it.
Order of task handover
The handover of tasks between the institute’s functional nodes is formalized. Every handover is accompanied by a document of a set format with metadata (date, source, recipient, type of task, priority, subject, current status), and the document is placed in a shared handover folder under a name that follows a single scheme.
This requirement performs the same function as an audit log in a banking system: every movement of a task from one executor to another is recorded so that the full chain can be reconstructed. In the event of an error, a dispute or a regulatory request, it is possible to trace who accepted, processed and passed on which task, and when.
In a multi-agent environment where the functional nodes may be autonomous, a formalized order of handover is the only way to keep the overall process under control. Without it the agents’ work degenerates into collective noise in which a result cannot be attributed to its source.
The source of truth for metrics
Every metric by which the institute evaluates its own work has one authoritative point of computation, fixed in a register of sources of truth. No autonomous module has the right to compute a metric on its own or to substitute the results of its computation.
This requirement arises from the nature of autonomous systems: a module that optimizes its own behavior against a metric has a built-in incentive to interpret the metric in its own favor. If it is allowed to compute the metric itself, in the long run the results will drift systematically in the module’s favor, and not necessarily through malice: that is how the structure of incentives works.
A single source of truth for each metric, protected from modification by the autonomous corps, removes this problem by design: modules may read metrics but may neither compute nor change them. This technical separation of functions follows the same principle that in science separates the experimenter from the observer.
Separation of lines of activity
The institute conducts several lines of activity with different audiences, regulatory regimes and registers of language, and the discipline of work requires that they be separated both organizationally and technically.
The separation is maintained by an automatic check of every publication for signs of another line before it is released. Content that fails the check is not published automatically and is escalated to the human node for manual qualification.
This requirement arises from practice with an autonomous content executor: without such separation, an autonomous module trained on a mixed corpus of materials from different lines can unintentionally carry the vocabulary or references of one line into the publications of another. In conversation with regulators, corporate clients and the academic community such a transfer is costly.
The separation makes the work in each line an independent discipline with its own vocabulary, sources and system of checks. The very structure of an organization with agent execution, which speaks to several audiences at once, requires it.
One principal measure of quality
Each line of the institute’s activity has its own system of quality measurement: a primary metric and auxiliary indicators. The metrics of different lines are neither added together nor compared with one another: they assess different kinds of activity by different criteria.
The principle of one principal measure of quality means that in each line one principal numerical assessment is defined by which changes are accepted or rejected, and the auxiliary indicators serve only for interpretation.
This requirement follows from the impossibility of optimizing against several metrics at once, a known result of multi-criteria optimization theory: an attempt to improve all indicators simultaneously leads to a compromise that maximizes none of them. A single principal metric per line makes the work meaningful and verifiable.
The formulas and weights of the auxiliary metrics are fixed and protected from modification, and any change to them requires an ADR with a rationale. This strong procedural requirement keeps the system from drifting its metrics in the executors’ favor.
Applying the principles to the institute itself
The institute applies the principles listed above both to the products it develops and to its own operations; this is the requirement of recursive self-application of the discipline.
An institute that declares the principle of a protected zone for the systems it develops must have such a zone in its own work. An institute that requires a single source of truth for metrics from autonomous modules must observe that requirement for its own indicators. An institute that separates lines of activity in the design of its products must observe that separation in its own communication.
The requirement is a strong one, because most organizations declare design principles for the products they develop but do not observe them in their own operations. For the institute such a discrepancy would destroy its doctrinal position: an organization with agent execution cannot be sold convincingly to a corporate client if the seller’s own work is organized without its principles.
The institute deliberately takes the opposite path and applies the principles recursively to its own work, in order to obtain the closest agreement between declaration and practice. This demands an operating discipline that most research and commercial organizations do not have.
What is not published
The institute publishes the principles of its work, that is, the methodology, the discipline and the rationale of its decisions, but it does not publish the individual ADR, for reasons of several kinds.
Some ADR contain trade secrets, that is, details of implementation that give a competitive advantage; publishing them would remove the advantage without any compensating benefit.
Some ADR contain operational details of infrastructure, such as configurations, the names of components and schedules of work. Publishing them would create a map of the infrastructure for possible hostile action, so keeping them closed is part of compliance by design in the field of information security.
Some ADR concern lines of activity protected by confidentiality obligations toward clients and partners, and publishing them would breach the institute’s obligations to its counterparties.
Some ADR concern activity governed by professional privilege, such as attorney-client, audit or medical confidentiality, in cases where the institute works with such data.
These restrictions do not contradict the institute’s principle of transparency, which concerns methodology, the rationale of decisions and the verifiability of results. Transparency does not mean disclosing operational details, competitively significant information or protected data of third parties, and the line between the public and the closed is drawn clearly: the methodology is open, the implementation is protected.
Access to closed materials
Institutional partners that conclude a cooperation agreement with the institute receive access to the details of specific ADR to the extent the cooperation requires; access is formalized by a non-disclosure agreement with a fixed scope of information to be transferred.
Academic partners working on joint research receive access to the ADR that have scientific value, on the terms of scientific publication with attribution of authorship to the institute.
Regulatory authorities acting within their powers receive access to ADR in the manner established by law, where legal grounds exist.
Inquiries about access to closed materials go to info@isslab.ru, with the subject and the nature of the request stated.
Closing provision
The institute does not set itself the task of convincing the institutional environment that the transition is inevitable, because that inevitability does not depend on persuasion. Its task is to provide the institutional environment with a design in which the transition becomes a governed event instead of a destructive one.
The discipline of the institute’s work does not follow from technological fashion or from marketing positioning. It follows from the nature of work with autonomous computing systems: an environment in which memory is distributed, responsibility is centralized, and errors are reproducible and cascading. In that environment the practice of ADR and the principles connected with it are the condition of the work being possible at all.
Without them the institute could not keep its declared doctrine of an organization with agent execution in agreement with its own operating practice, and keeping that agreement remains the institute’s main long-term obligation.
Institutional capital that adopts this design in time enters the new configuration while keeping its historical form. Institutional capital that postpones that entry enters on the terms of an environment that by then has formed without its participation.
The institute offers a design in which the transition to autonomous executors becomes governable: a person signs the rule, the admissibility of an action is proved before execution, and the decision is recorded so that an outsider can check it.
Checking inside the customer’s perimeter, proof before execution, a record for an outside reviewer
Checked: 18 October 2026: the validity and details of the legal acts and standards named on this page, against primary sources.
The doctrine is the position from which the institute’s method, its research program and MITR follow. A conversation about how it applies to a particular organization begins with a message to the scientific director or a letter to the institute with the subject “Doctrine”. The method is described on the page “The method of system synthesis” (in Russian), and the research program on the page “Research program”.
Write to the scientific directorE-mail info@isslab.ru
Autonomous non-profit organization “Research Institute of System Synthesis”, Moscow. The Russian page “Доктрина управляемого перехода” is the original text, and this page follows it.