Suradnjom s tvrtkom Theorem istraživači su pokazali da veliki jezični modeli mogu generirati formalne dokaze u velikom opsegu. Uz pomoć modela Claude dokazana su sigurnosna svojstva na razini RISC-V sklopnog koda u više od 100 stvarnih open-source biblioteka.
Prema njihovim saznanjima, to je prvi takav opsežan projekt primjene umjetne inteligencije za formalnu verifikaciju proizvodnog softvera na razini sklopnog koda. Tijekom izrade dokaza Claude je otkrio greške koje su godinama ostajale neotkrivene unatoč bilijunima testnih pokretanja.
Autori predviđaju da će, kako sposobnosti modela napreduju, formalna verifikacija postati sastavni dio sigurnog razvoja softvera.
