Как работает MITR

Формальный аппарат

Каждый контракт переводится в формулы разрешимой логики QF_UFLIA — бескванторной логики с неинтерпретируемыми функциями и линейной целочисленной арифметикой по классификации SMT-LIB, библиотеки задач выполнимости формул в теориях (SMT). Решатель проверяет выполнимость конъюнкции наблюдённых посылок и отрицания условия безопасности. Невыполнимость означает, что при этих фактах нарушить условие нельзя, и действие допускается; посылки, на которых держится доказательство, записываются в квитанцию. Выполнимость даёт контрпример — состояние, согласное с наблюдениями и нарушающее условие; по нему MITR называет агенту недоказанные ветви контракта и условия исправления. Проверка в этой логике всегда завершается: задача разрешима и принадлежит классу недетерминированно полиномиальных задач (NP), где она NP-полна, а полиномиальный алгоритм для неё не известен. На узких спецификациях реальных вызовов решатель отвечает за миллисекунды, и в MITR медиана времени решения составляет 1,08 мс (24.10.2026, 20 контрактов, 1 000 решений).

Пример условия безопасности для платёжного агента — иллюстрация формы, а не контракт из каталога MITR:

;; сумма не превышает остатка суточного лимита роли,
;; инициатор платежа не совпадает с утверждающим,
;; счёт получателя — в списке проверенных
(assert (and
  (<= (+ spent_today_kop amount_kop) role_daily_limit_kop)
  (not (= initiator_id approver_id))
  (verified_recipient recipient_account_id)))

Криптографическая цепь квитанций строится последовательно: хеш каждой новой записи вычисляется от хеша предыдущего звена и канонического представления текущего события. Любая правка, удаление, вставка или перестановка строки немедленно нарушает сходимость всей последующей цепи. Чтобы исключить полный пересчёт журнала владельцем сервера, вершина цепи ежесуточно закрепляется у независимого внешнего свидетеля времени.

Граница гарантии

• MITR гарантирует математическую корректность (Soundness): ни одно разрешённое действие не нарушает заданное правило, тогда как полноту перевода внешней нормы в контракт обеспечивает человек, а квитанция называет применённую спецификацию.
• Доказательство опирается на переданные наблюдения: исходные факты поставляют датчики и учётные системы организации, поэтому для каждого параметра нужен независимый наблюдатель, в отсутствие которого выставляется статус «не измерено», а не «безопасно».
• Неотвратимость проверки обеспечивается установкой: ключи от целевых систем выдаются MITR, а агенту остаётся право запросить проверку. Агент, у которого есть собственные ключи, обходит любой слой контроля, поэтому свойство «мимо не пройти» проверяется на установке, а не обещается.
• Вторая языковая модель в решении MITR не участвует: вердикт представляет собой детерминированный расчёт по правилу на обычном процессоре без вызова вероятностной нейросети.

Что измерено и где это проверить

Автономная некоммерческая организация (АНО) «Научно-исследовательский институт (НИИ) системного синтеза», редакция от 25 октября 2026 года: все приведённые числа сопровождаются датой приборного замера на сервере MITR. Проверено по первоисточникам: 25.10.2026 (действие стандарта ГОСТ Р 34.11-2012), а перечень разработок и формы партнёрского участия описаны на страницах «Разработки» и «Инвесторам и партнёрам».