In a minute
The program is a research program in the formal verification of the actions of artificial intelligence for regulated industries: a solver checks every irreversible action of an agent against a set of axioms before it is executed. Phase 0 is in operation: MITR (the institute’s proven-action system) has run continuously since 24 April 2026, all 20 of its contracts have been in enforce mode since 24 October 2026, and its receipt chain has been kept since 16 September 2026. Phase I adds an independent observer for every fact a rule depends on, closes the three gaps named by the attack set and runs a thirty-day pilot at an outside customer; the later phases turn the method into a standard package for sector regimes. The guarantee is stated together with its boundary: the solver guarantees that a permitted action does not violate the formalized policy, while the completeness of the translation of a norm into axioms stays with an authorized specialist. The program is open to pilot partners in regulated sectors, to institutional partners and investors, and to research bodies; the terms of entry are set in a conversation with the scientific director.
Subject of research, market window, phases of work
The institute carries out a research program in the formal verification of the actions of artificial intelligence for regulated industries. Its subject is a layer of trust built over an autonomous agent: every irreversible action is translated into a formal specification and is checked mathematically against the given axioms before execution.
One of the defining properties of such a system is verifiable user sovereignty: the agent’s actions provably conform to the declared interests of the end user and cannot be covertly subordinated to the interests of the platform operator.
Over the next 12 to 18 months a regulatory and market vacuum is forming in the Russian Federation between the embedded agents of large platforms and foreign models that are becoming unavailable. Professional categories of users are being pushed into that vacuum: users for whom platform optimization is incompatible with their fiduciary, professional or regulatory responsibility.
The program answers that vacuum with a standard engineering design and a methodology for deploying user-sovereign agents inside the customer’s perimeter, on an open technology stack, without being tied to a platform.
The program is accompanied by a production reference implementation, MITR, which has run continuously since 24 April 2026. MITR constitutes Phase 0 of the program and serves as the operating environment in which the institute checks invariants, formalizes policy and measures behavior. The scientific task of Phase I is to carry the engineering principles of MITR from an imperative implementation into a formalized one that is verified with the apparatus of satisfiability modulo theories (SMT).
Formal verification of the actions of autonomous agents; neurosymbolic artificial intelligence; satisfiability modulo theories (SMT) in quantifier-free linear integer arithmetic with uninterpreted functions (QF_UFLIA); sovereign micro-prover; deductive verification with AstraVer; local deployment inside the customer’s perimeter; 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 (FSTEC of Russia); GOST R 56939-2024; GOST R 57580
Element of scientific novelty
The prevailing approach to the safety of autonomous systems built on large language models relies on behavioral alignment: reinforcement learning from human feedback (RLHF) and Constitutional AI (training a model against a written set of principles). Both depend on the ability of the probabilistic model itself to interpret and observe principles written in text, and so neither gives a formal guarantee. They remain exposed to adversarial attacks, to hidden drift of behavior and to logical contradictions in policies. No increase in the volume of training turns a behavioral tendency into a proof.
The institute builds a different approach: the control layer over an autonomous agent works as an axiomatic normative environment that is checked by formal methods. The interests declared by the user, regulatory requirements and corporate policies are formalized as axioms; every action is translated into a strictly typed specification and is checked by an SMT solver before execution. Actions without a mathematical proof of admissibility are rejected by a software barrier before execution.
The boundary of the guarantee is stated with full mathematical rigor: MITR guarantees soundness, which means that a permitted action does not violate the formalized policy. The correctness of translating a norm into axioms, that is, the semantics, stays with an authorized specialist. Grammar-constrained generation (constrained decoding) guarantees only the syntax; protection against semantic drift is achieved by translating the specification back into natural language for a human audit before the solver is run. MITR leaves the final decision with the responsible specialist and gives that specialist a verifiable proof for every step.
The fundamental difference from known work lies in the object and the moment of checking. Formal verification of program code applies solvers to static artifacts; the program applies them to the dynamic stream of an agent’s commands, before execution and asynchronously. Constrained decoding is responsible for the syntax of the output; the program deals with the semantics and the logical consequences of an action. The constitutional approach aligns behavioral tendencies; the program removes the technical possibility of executing an action that is not derivable from the axioms.
The computational complexity of the method is assessed without embellishment. The strength of the approach lies in checking an isolated, strictly typed predicate instead of the whole textual context. The satisfiability problem in the chosen theory QF_UFLIA is decidable, so a check always terminates, and it belongs to the class of nondeterministic polynomial time (NP): it is NP-complete. There is no guarantee of polynomial time, and in the worst case exponential growth is possible. On narrow practical specifications that growth is contained by the heuristics of modern solvers, conflict-driven clause learning with theory reasoning, CDCL(T), and comes down to delays of milliseconds. The industrial scalability of the SMT approach is confirmed by the practice of global operators at the level of a billion checks a day (Amazon’s Zelkova service).
The institute’s program brings these components together into a single standard package suitable for local deployment inside the perimeter of corporate and state customers under the requirements of Russian law.
Market window
The institutional environment of the Russian Federation is passing through a phase of rapid formation of its own legal regime for the use of autonomous systems based on artificial intelligence. Two factors act at the same time and together form a segment of professional demand for checking an agent’s actions inside the customer’s perimeter.
The first factor is the ecosystem optimization of large domestic platforms. Products built on large language models by the Russian technology majors are by construction subordinated to the logic of keeping the user inside the operator’s own system: the business model presupposes the capture of attention and the cross-selling of services within it. For a large share of corporate and professional scenarios this mode of operation is incompatible with the requirements of confidentiality, fiduciary responsibility and independence of judgment.
The second factor is the gradual restriction of access to foreign models in professional scenarios. Data localization requirements, the regulation of “trusted” and “sovereign” artificial intelligence now in preparation, the restrictions for critical information infrastructure facilities and the legal regime of professional privilege (attorney-client, medical, audit) all bear on it. Together they make the use of external cloud application programming interfaces (API) in a corporate network legally risky or outright unacceptable.
At the intersection of these factors a segment of professional users is forming: banks and financial organizations with fiduciary responsibility; medical organizations; law firms and bar associations; operators of critical information infrastructure; state information systems; corporate compliance and internal audit units. The institute’s program answers this segment with MITR, through which the action of any agent, the organization’s own or a third party’s, passes before execution and is admitted only with a proof, inside the customer’s perimeter and under the customer’s rules.
Technical base
The program rests on a mature base of open solutions for the language and orchestration apparatus and creates its own verification core, which is the protectable result of the institute’s intellectual activity.
The language apparatus consists of open large language models for local deployment, including compact domestic models adapted to Russian; the module is replaceable, which keeps the program independent of any generation of models and of any single supplier.
The orchestration apparatus consists of lightweight agent runtimes (CrewAI, AutoGen, LangGraph). The institute’s fundamental addition is a built-in layer of formal policy verification that existing orchestrators lack: every tool call is translated into first-order logic and checked before execution.
The verification core is the institute’s own development: on the research bench (in Russian) the check is performed by the solver Z3 (Microsoft Research) as the reference for the method. The target result is a sovereign trusted micro-prover: a compact implementation of the decision procedure for the decidable theory QF_UFLIA in a trusted environment, with no dependence on foreign libraries in the core.
The compactness of the code opens the way to deductive verification of the prover itself with the instruments of the Ivannikov Institute for System Programming of the Russian Academy of Sciences: the AstraVer platform with Frama-C and Why3, and specifications in a formal contract language for C programs (ACSL). The same route leads to conformity assessment by the assurance levels of FSTEC of Russia Order No. 76 in secure software development under the Russian national standard (GOST R 56939-2024). The protocols of transition and the states of safe failure are checked in the temporal logic of actions (TLA, TLA+); the deep correctness of the decision procedure and of code generation is established by interactive proof (Rocq, formerly Coq). The solver core runs on standard server processors and needs no specialized hardware.
Phases of the program
The program unfolds in four consecutive phases, and each phase fixes tangible results suitable for institutional and scientific review.
Phase 0. Production reference implementation (current)
The goal of the phase is a working MITR in the institute’s own loop, in continuous operation.
MITR has run continuously since 24 April 2026 on the institute’s internal bench and checks the actions of the institute’s own software agents: coding agents, services and connections over the Model Context Protocol (MCP). Since 24 October 2026 all 20 contracts have been checked by the solver and run in enforce mode. The rules are stored as data and are applied without rewriting the program. The receipt chain has been kept since 16 September 2026 and is anchored once a day by an external time witness.
Measured: 6,414 automated tests with no failures (the nightly run of 25 October 2026), and an adversarial set of 157 cases with no attack missed and no false refusal (24 October 2026). The replay of decisions by the checker for an outsider matched 5,079 of 5,079 (25 October 2026). The agents’ memory carries the provenance of every record, and the decision log is append-only.
The tangible results of the current phase include a working prototype of an agent runtime with built-in verification layers that withstands adversarial attacks on policy. Methodological documentation in the form of design records has been created, and a numbered roadmap of research and development work has been drawn up.
Two things the initial phase does not provide: an independent observer for every fact on which a rule depends, and a measurement at an external customer. They form the content of Phase I.
Phase I. Fact observers, full coverage and an external pilot
The goal of the phase is proof-based checking on facts taken by independent observers, for the whole class of irreversible actions, and the first pilot in an external loop. The phase is open to the grant programs of development institutions and to partner funding.
The content of the phase is five research milestones; each is closed by a written decision or a scientific preprint, and by tests:
- Fact observers: one deterministic observer for every fact of a contract; where the observer is absent, the fact receives the status “not measured” and the action is not admitted.
- Checking the form of a request between the model’s output and the executor: a request with distorted parameters of an irreversible action is rejected before the check on the merits.
- Closing the three gaps in the rules that the adversarial set names, and extending proof-based checking to the whole class of irreversible actions, with latency measured.
- Checking the reliability of samples drawn from the agent’s long-term memory, with the confidence in each record taken into account, and a regular review of that confidence with a log of changes.
- A thirty-day pilot in an external loop with a stated share of false stops.
The tangible results of the first phase are a formalized specification of the package fit for submission to review, and MITR with fact observers and model checking of safe-failure protocols, running in an isolated environment. They also include the first technical reports and scientific preprints, and registration of the software components in the register of domestic software.
Phase II. Standard package and pilot deployments
The goal of the phase is to shape the methodology into a reproducible standard package suitable for deployment inside the customer’s perimeter, and to carry out pilot deployments with the first institutional partners in the relevant segments.
The tangible results of the second phase form a standard software package with accompanying documentation and deployment tooling. Pilot deployments with the first partners take place in the segments most sensitive to the requirement of user sovereignty: professional legal practice, medical organizations and corporate compliance units. The first edition of a base of formal axioms for standard sector regimes (Federal Law No. 187-FZ, FSTEC of Russia Order No. 117, GOST R 57580) is produced, and the specific facilities of the first pilots are certified under information protection requirements.
Development of the institute’s own compact solver for the QF_UFLIA logic begins, with deductive checking of its code on the instruments of the Ivannikov Institute for System Programming of the Russian Academy of Sciences (AstraVer), on the way to conformity assessment by the assurance levels of FSTEC of Russia.
Phase III. The institute as the holder of a standard
The goal of the phase is to establish the institute as the methodological and expert center for building user-sovereign agents in the Russian jurisdiction.
The tangible results of the third phase include a base of formal axioms covering the main sector regimes and sector standards, with a regime of regular updating. They also include programs of continuing professional education for corporate and state specialists, and the institute’s participation in forming sector and national standards for the design of autonomous systems with formal guarantees of correctness.
Certification of the checking core by the assurance levels of FSTEC of Russia belongs to this phase as well.
Commercialization
The commercial part is conducted by an operating company that receives a license to the institute’s developments. The revenue model, the order of entry into the project and the use of funds are set out on the page “Investors and partners”, and the first transaction is a paid pilot with an industry customer.
A separate line is the transfer of knowledge: programs of continuing professional education for the customer’s specialists, participation in forming sector standards, and expert opinions for regulators. This line has commercial value of its own and at the same time serves as the mechanism by which a professional community forms around the institute’s methodology.
Risks and how they are contained
The research program identifies in advance four structural categories of risk and the engineering mechanisms for reducing each of them step by step.
Regulatory risk
A possible tightening of certification requirements for autonomous systems in the Russian Federation may complicate the licensing of independent developments. The program relies on this very dynamic as the foundation of its market position.
The apparatus of formal verification is by its nature a direct instrument for passing state review, and it gives the reviewing authority a methodological model for future standards of trusted artificial intelligence. The scientific director’s practice as an attorney and in audit helps to take legal norms into account directly in the design of the system.
Technological risk
The application of SMT solvers to problems of unbounded complexity in theory meets a computational explosion. In the design of MITR this risk is structurally limited by handing the solver only a strictly typed, isolated predicate.
The theory QF_UFLIA is decidable, so a check always terminates, and it is NP-complete: there is no guarantee of polynomial time, but on narrow practical specifications the exponential growth is contained by the solver’s heuristics, and a check takes milliseconds. Scalability is confirmed by industrial practice at the level of a billion checks a day.
Competitive risk
The probability that large Russian platforms quickly enter the segment of user-sovereign agents is structurally limited. The commercial model of the large platforms rests on holding the user’s attention and collecting telemetry inside their own cloud environment. Releasing an autonomous agent physically disconnected from an external operator runs against their direct benefit and leaves the segment to a specialized independent institute.
Reputational risk
The institute deliberately avoids public competition with the existing platform players on their own ground of mass consumer products. The program is positioned as institutional-grade infrastructure software that complements generative language models with a deterministic checking barrier. This approach strengthens the institute’s business reputation and its ability to work with regulators and industry associations in the neutral standing of a methodological center.
Criteria for entering the program
The program is open to three categories of participants that correspond to its current phase.
Pilot partners from the relevant industries are organizations for which the requirement of user sovereignty is a direct operational matter: professional practices with fiduciary responsibility, medical and educational organizations, corporate compliance units and state information systems. The form of cooperation is a joint pilot deployment, with both sides ready for close working communication while the package is being configured.
Institutional partners and investors regard the program as a long-term position in a forming segment. The form of cooperation is a conversation with the scientific director and a confidentiality agreement; the order of entry is described on the page “Investors and partners”.
Academic and sectoral research bodies work in formal verification, multi-agent systems and the legal foundations of autonomous technologies. The form of cooperation is joint research programs, expert councils and participation in dissertation work.
Closing provision
The institute’s program is carried out in a form in which every stage leaves a tangible trace: a working prototype, a formal specification, published artifacts, pilot deployments. This lets regulatory, academic and investment reviewers judge the state of the program by verifiable tangible results.
Phase 0 has already been presented in working form, while Phase I is open to state support and to qualified expert assessment. Phases II and III shape the long-term horizon of the institute as a methodological center for the design of autonomous systems with formal guarantees of correctness.
Inquiries of a general nature are not considered.
Checked: 25 October 2026: the validity and details of the legal acts and standards named on this page, against primary sources.
Entry into the program begins with a conversation: a pilot partner describes its task and its site, an institutional partner or an investor agrees the terms of a confidentiality agreement, and a research body proposes a joint program. The first step is a message to the scientific director or a letter to the institute with the subject “Program”; the doctrine from which the program follows is on the page “Doctrine of the governed transition”.
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.