Мой очередной AI-moment

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

Ну как завайбил, написал спеку и перекидывал между двумя модельками с фразами «ты инженер по формальной верификации — реализуй» и «ты параноик — проведи аудит и найди сговор разработчиков».

Вначале в Lean описал формальную спецификацию в абстрактных типах и доказал все теоремы безопасности (2-3 раунда аудитов, 2 дня фоновой работы агентов). Затем в том же Lean написал вычислимую реализацию уже с конкретными типами данных (set, map, array) и доказал эквивалентность с исходной абстрактной моделью (1 день фоновой работы). Бонусом сериализацию в SQL и обратно, с проверкой логической целостности, что бы где-то хранить все доступы и ресурсы.

На выходе Lean генерирует код на C, который можно слинковать через FFI с Go или Rust, но я собрал в C++ микросервис.

Производительность на одном ядре:
200-250к обращений в секунду на проверку доступа
150к изменений/сек при базе в 10к пользователей
15к изменений/сек при базе в 100к пользователей (тут можно ещё оптимизировать)

Доказательства: Gemini Flash
Написание неформальной спеки и аудиты: Claude Opus

Если бы раньше меня спросили, сколько будет стоить формально верифицированный IAM сервис, я бы оценил такой проект минимум в 6-9 месяцев работы команды из 2-3 человек с зарплатами от $250k в год на каждого.

Начинается эпоха vibe-proving?