Claude і формальна верифікація: що довели для 123 бібліотек

Найслабше місце вайб-кодингу часто з’являється після красивого демо. Сторінка відкривається, кнопка працює, помічник пише «готово». Але як зрозуміти, чи витримає програма незвичайні дані? Свіжа робота Anthropic дає привід поговорити про інший рівень перевірки — і про те, чого варто вимагати від ШІ вже у невеликому проєкті.

Що саме оголосила Anthropic

22 жовтня 2026 року Anthropic повідомила про спільну з Theorem роботу: Claude побудував формальні докази для 239 точок входу у 123 відкритих бібліотеках. Докази стосуються визначених властивостей скомпільованого коду; їх перевіряє ядро Rocq. Це результат команди авторів, який редакція самостійно не відтворювала.

Основний експеримент має чіткі межі: однопотокові статичні програми для RISC-V/Linux, фіксований бюджет пам’яті та вхідні дані менші за 64 МБ. Висновок залежить від специфікації, моделі виконання і перевіряча. Він не означає, що всі 123 бібліотеки позбулися будь-яких помилок на всіх платформах. Першоджерело й обмеження дослідження →

Почни з правила, яке можна порушити

Уявімо навчальну гру з магазином спорядження. Герой має 50 монет, меч коштує 40. Перша покупка проходить, залишається 10. Це один успішний приклад. А що станеться після подвійного натискання, від’ємної кількості товару або завантаження старого збереження?

Для такого проєкту корисно записати окремі правила: баланс не стає від’ємним; кожна підтверджена покупка додає рівно один предмет; повторне відкриття вікна не повторює списання. Це наш умовний приклад постановки задачі, а не результат експерименту Anthropic.

Слова «гра працює» приховують багато різних вимог. Правило про монети не перевіряє зручність керування, доступність для людей зі слабким зором чи збереження прогресу після перезапуску. Коли вимоги названо окремо, легше побачити прогалини у звіті.

Як читати відповідь агента про перевірки

Проси чотири речі: що перевіряли, на яких даних, що фактично отримали та де закінчується перевірка. Фраза «помилок не виявлено» без цих деталей дає мало інформації. Список тестів також не замінює їхнього виконання.

Для маленької гри можна почати з таблиці сценаріїв у звичайному текстовому файлі. Поруч із кожним правилом записати нормальний випадок, граничний випадок і спробу некоректної дії. Коли змінюєш магазин, повертайся саме до цих сценаріїв. Для сайту аналогічним правилом може бути «користувач редагує тільки власний запис».

Готове завдання для ШІ

Цей редакційний шаблон допомагає замовити предметну перевірку. Сам по собі він не запускає інструмент формальної верифікації.

Перевір конкретну властивість мого проєкту: [сформулюй правило].
1. Вкажи, які файли та сценарії стосуються цього правила.
2. Назви припущення, без яких висновок не діє.
3. Запропонуй приклад, що міг би порушити правило.
4. Виконай доступну перевірку й покажи фактичний результат.
5. Окремо переліч, що залишилося неперевіреним.
Якщо це звичайні тести, так і назви їх. Не називай пояснення формальним доказом. Не змінюй правило лише заради успішної перевірки.

Для новачка і для розробника

Якщо ти тільки починаєш, візьми одну важливу дію: покупку, збереження або публікацію. Попроси пояснити, що може піти не так, і разом перевір шість конкретних випадків. Краще розуміти одну таку дію, ніж отримати незрозумілий звіт на двадцять сторінок.

Якщо працюєш професійно, до кожного висновку додай версію коду, середовище й команду відтворення. Після зміни залежностей або алгоритму старий результат потребує перегляду. Окремо перевір, чи агент не послабив умову, яку мав довести.

Для власної браузерної гри почни з мінікурсу зі створення гри з ШІ. А якщо сайт уже існує, допоможе практичний розбір перевірки коду агентами. Найкорисніше питання до помічника після «готово»: «Покажи, за якими спостереженнями ти зробив цей висновок».

Ще з цієї добірки

• Project Swap: ШІ вміє торгуватися, але чи розуміє, чого ти хочеш?
• Чому ШІ забуває важливе: JAM і пам’ять під конкретну задачу