DailySafe · Технологии и исследования
Ежедневные инструктажи и подтверждения работы влияют на реальных людей. Поэтому важно установить происхождение записи, действовавшие правила, последовательность исправлений и возможность последующей независимой проверки.
Мы соединяем практический опыт строительных объектов с математическими методами, чтобы точнее определять смысл событий и проверять результаты.
6 направлений
6 групп доказательств
76 успешных специальных тестов
Результат CI от 4 ноября 2026 года
Аналитический отчёт Вадима Акуленко, PhD, рассматривает десять интервью об учёте рабочего времени на стройках, заводах и в других рабочих условиях. Выводы не претендуют на статистическую репрезентативность.
Открыть результаты исследования →Шесть направлений связывают практические задачи охраны труда с формальными моделями и программными механизмами.
Участие в TBM, рабочие часы, возражения и исправления рассматриваются как связанные, но самостоятельные события. Важна не только итоговая цифра на экране, но и происхождение решения.
В backend существуют механизмы и испытания происхождения данных и истории исправлений.
Если новые правила задним числом применить к вчерашнему подтверждению, смысл записи изменится. Поэтому рассматривается закрепление версии, содержания и времени действия правил.
Есть формальные теоремы Lean 4 о закреплении правил, а также программные испытания целостности снимков правил и отказа в ретроактивном TBM.
Правила выражаются в математической модели; система проверки доказательств устанавливает выполнение определённых инвариантов модели. Среди них — закрепление правил, происхождение доказательств, сохранение прежних элементов при добавлении и согласованность переходов.
Доказаны свойства математической модели, а не автоматически всего приложения, базы данных или промышленного сервера.
Подписанные контрольные точки и повторный расчёт истории используются для выявления определённых типов подмены, удаления и отката записей.
4 ноября 2026 года прошли 76 специальных программных тестов M4/M5, включая отдельный процесс-свидетель и автономную проверку. Это не свидетельство промышленного развёртывания на независимом сервере.
Полномочия руководителя одной организации не должны распространяться на чужой объект. Подтверждение работником конкретных часов не должно автоматически подтверждать их изменённое значение.
В техническом реестре описаны отрицательные и положительные тесты API и семантики базы данных.
Исследуются связи между учётом часов, решением руководителя, возражением работника и исправлением. Несколько заявок затрагивают расчёты на основании доказательств и локализацию споров.
Тематика патентной заявки не равнозначна выданному патенту или наличию всех соответствующих функций в приложении.
Для каждого утверждения указано, на каких документах или испытаниях оно основано и что именно они подтверждают.
Описаны инварианты, сценарии API/DB и границы испытаний истории, полномочий и подтверждения значений.
Граница доказательства: Технический отчёт, не сертификат работающей промышленной системы.
Доказательства · E-01 →Теоремы Lean 4 A2_policy_pinning_strict и A3_deny_retroactive_strict сопоставлены с задачами продуктовой политики.
Граница доказательства: Доказательство модели не означает формальной верификации всего продукта.
Доказательства · E-02 →Систематизированы теоремы A5_append_only, A0_event_provenance_strict, pipeline_consistent и другие.
Граница доказательства: Соответствие модели реальным FastAPI/PostgreSQL проверяется отдельно.
Доказательства · E-03 →76/76 тестов прошли в CI: подмена, удаление, откат, отдельный HTTP-процесс, открытый ключ и запрет заднего числа.
Граница доказательства: Испытана программная среда, а не развёртывание на отдельно управляемом промышленном сервере.
Доказательства · E-04 →Описаны проверки чужой организации, действительности полномочия в момент действия и изменения уже подтверждённого значения.
Граница доказательства: Охватывает определённые пути API/DB, не любую возможную угрозу.
Доказательства · E-05 →Сверяет отобранные заявки DailySafe с закрытым реестром подачи.
Граница доказательства: Заявка не означает выдачу патента или реализацию всех заявленных технологий.
Доказательства · E-06 →Номера и темы заявок, связанных с историей событий, версиями правил, расчётами и проверкой доказательств, собраны в отдельном каталоге. Подача заявки не означает выдачу патента или наличие всех функций в приложении.
Открыть каталог заявок →Математически доказанное свойство модели, успешный тест программы и гарантия, включённая на действующем объекте, — разные уровни подтверждения. Мы не смешиваем их.