Коротко
За заявою розробників, математичні докази перевірив інструмент Rocq. Гарантії стосуються лише визначених умов і властивостей програм.
Anthropic заявила про застосування Claude у спільному з Theorem проєкті формальної перевірки програмного забезпечення. За повідомленням РБК-Україна від 23 жовтня з посиланням на Interesting Engineering, робота охопила 123 бібліотеки з відкритим кодом.
У проєкті модель перетворювала наявні фаз-тести на математичні специфікації та генерувала докази для 239 точок входу. Як повідомляють розробники, вони стосувалися відсутності збоїв за визначених умов. Згенеровані докази перевіряв окремий інструмент Rocq.
Під час роботи, за заявою компанії, виявили приховані дефекти, зокрема помилки доступу за межі дозволеної пам’яті та проблему в XML-парсері libexpat. У повідомленні також ідеться про виправлення моделлю знайдених помилок і створення доказів для оновленого коду.
Anthropic застерігає, що формальна перевірка не робить програму повністю безпомилковою. Гарантії охоплюють лише властивості, вхідні дані й припущення конкретного доказу. Описаний підхід наразі стосується однопотокових, статично зв’язаних програм RISC-V у змодельованому середовищі Linux.