Исходные репозитории GitHub закрыты. Здесь приводятся разрешённые к публикации результаты, даты и ограничения проверок. Эти сведения не заменяют исходные журналы испытаний или независимую техническую экспертизу.
Доказательство свойств математической модели, успешные программные тесты и проверка промышленной системы — не одно и то же.
Что подтверждено: Описаны инварианты, сценарии API/DB и границы испытаний истории, полномочий и подтверждения значений.
Ограничения: Технический отчёт, не сертификат работающей промышленной системы.
Что подтверждено: Теоремы Lean 4 A2_policy_pinning_strict и A3_deny_retroactive_strict сопоставлены с задачами продуктовой политики.
Ограничения: Доказательство модели не означает формальной верификации всего продукта.
Что подтверждено: Систематизированы теоремы A5_append_only, A0_event_provenance_strict, pipeline_consistent и другие.
Ограничения: Соответствие модели реальным FastAPI/PostgreSQL проверяется отдельно.
Что подтверждено: 76/76 тестов прошли в CI: подмена, удаление, откат, отдельный HTTP-процесс, открытый ключ и запрет заднего числа.
Ограничения: Испытана программная среда, а не развёртывание на отдельно управляемом промышленном сервере.
Что подтверждено: Описаны проверки чужой организации, действительности полномочия в момент действия и изменения уже подтверждённого значения.
Ограничения: Охватывает определённые пути API/DB, не любую возможную угрозу.
Что подтверждено: Сверяет отобранные заявки DailySafe с закрытым реестром подачи.
Ограничения: Заявка не означает выдачу патента или реализацию всех заявленных технологий.
Первичные материалы хранятся в закрытом архиве и могут быть предоставлены уполномоченным проверяющим после согласования условий доступа.