Anthropic ادعای بزرگی دربارهٔ یکی از قدیمی‌ترین آرزوهای علوم رایانه مطرح کرده است. این شرکت در پژوهشی که ۲۲ اکتبر منتشر شد می‌گوید Claude با کمک ابزارهای استارتاپ Theorem اثبات‌هایی صوری تولید کرده که نشان می‌دهد مجموعهٔ بزرگی از کدهای متن‌باز واقعی در شرایطی که خود توسعه‌دهندگان آزمایش می‌کنند از کار نمی‌افتند. راستی‌آزمایی صوری تاکنون به صنعت هوانوردی، هستهٔ سیستم‌عامل‌ها و نرم‌افزارهایی محدود بود که صرف سال‌ها کار متخصصان برایشان توجیه داشت. به گفتهٔ Anthropic، مدل‌های زبانی اکنون این کار را برای کتابخانه‌های معمولی هم مقرون‌به‌صرفه کرده‌اند.
نقطهٔ شروع، آزمون‌های فازینگ برنامهٔ OSS-Fuzz گوگل بود. فازر حجم عظیمی از ورودی‌های دست‌کاری‌شده را به یک نقطهٔ ورود می‌فرستد و هر ورودی را که باعث از کار افتادن برنامه شود گزارش می‌کند، از جمله خطاهای حافظه‌ای که AddressSanitizer تشخیص می‌دهد. چنین جست‌وجویی هیچ‌وقت کامل نیست. پژوهشگران هر آزمون را به یک گزارهٔ ریاضی تبدیل کردند: برنامهٔ کامپایل‌شده با هیچ ورودی کوچک‌تر از ۶۴ مگابایت از کار نمی‌افتد. اثبات این گزاره در دستیار اثبات Rocq بر عهدهٔ Claude بود و برای این کار از مدل‌های صوری Theorem برای دستورهای RISC-V و رفتار فرایندهای لینوکس استفاده شد.
طبق این گزارش، Claude ظرف چند هفته اثبات ۲۳۹ نقطهٔ ورود را در ۱۲۳ کتابخانه به پایان رساند. حجم کل اثبات‌ها حدود ۱۸۰ میلیون خط کد Rocq است و یک اثبات معمولی برای باینری‌ای با حدود ۱۸ هزار دستور به نزدیک ۶۰۰ هزار خط می‌رسد. به گفتهٔ شرکت، لازم نیست کسی این‌ها را بخواند، چون هستهٔ Rocq تک‌تک گام‌ها را به‌طور خودکار بررسی می‌کند. آنچه باید به آن اعتماد کرد محدودتر است: مدل‌های RISC-V و لینوکس، صورت دقیق قضیه‌ها و خود ابزار بررسی. این تضمین‌ها پیش‌فرض‌هایی هم دارند، از جمله اینکه برنامه به‌صورت باینری ایستا، تک‌رشته‌ای و با بودجهٔ حافظهٔ ثابت اجرا شود.
تلاش برای اثبات، کار شکار باگ را هم انجام داد. هر بار که Claude به خطایی قابل‌دسترس برمی‌خورد، کد را وصله می‌کرد و ادامه می‌داد و Anthropic می‌گوید این روند صدها باگ را آشکار کرد. از جملهٔ آن‌ها نوشتن خارج از محدوده در یک ابزار فشرده‌گشایی است که فقط با ورودی‌های حدود ۲۰ مگابایتی ظاهر می‌شد، خطای خواندن در یک رمزگشای تصویر که به فایلی ۶۴ مگابایتی و بیش از ۲ گیگابایت حافظه نیاز داشت، و کشف دوبارهٔ یک آسیب‌پذیری شناخته‌شده در libexpat. فازرها که معمولاً ورودی را به حدود یک مگابایت محدود می‌کنند، به‌ندرت به چنین مواردی می‌رسند.
آزمایش‌های جانبی از این هم فراتر رفتند. Claude مشخصات صوری قالب zlib را که در RFC 1950 تعریف شده نوشت و ثابت کرد پیاده‌سازی zlib در هستهٔ لینوکس با آن مطابقت دارد، این بار روی باینری‌های x86. همچنین با زبان Rust مفسری برای بخش بزرگی از پایتون ساخت، با ابزار Verus انطباق آن را با یک مدل دانشگاهی از CPython اثبات کرد و در ۹۹٫۹۵ درصد از ۱٫۷ میلیون برنامهٔ تصادفی رفتاری یکسان با CPython گرفت. به گفتهٔ شرکت، بررسی یک نرم‌افزار پرکاربرد خواندن PDF در یک هفته به اندازهٔ یک سال گزارش‌های معمول، نقص امنیتی پیدا کرد.
هزینه هنوز مانع اصلی است، چون برخی اثبات‌ها صدها میلیون توکن مصرف می‌کنند. Anthropic می‌گوید Claude Opus 5.5 نیمی از یک مجموعهٔ ۳۶ تکلیفی راستی‌آزمایی را با حدود ۴۰ درصد توکن کمتر از Opus 5 حل کرده و عامل‌هایی که فضای مشترکی از اثبات‌های قابل استفادهٔ مجدد داشتند ۱۷ درصد دیگر صرفه‌جویی کردند. Theorem قصد دارد این روند را به پروژه‌های متن‌باز دیگر هم عرضه کند و نقشهٔ راهی منتشر کرده که اکوسیستم Nix، از جمله glibc و OpenSSL و cURL، را هدف گرفته است.
Anthropic مدل‌های مورد اعتماد تازه، اثبات کامل آزمون‌هایی که به وصله نیاز نداشتند و مشخصات آزمون‌هایی را که اثبات نشدند منتشر می‌کند، اما هر چیزی را که ممکن است نقص‌های وصله‌نشده را لو بدهد نگه می‌دارد. شرکت تأکید می‌کند که اعتبار یک اثبات به مشخصات آن بستگی دارد: اگر مدل ماشین نادرست باشد، کد راستی‌آزمایی‌شده هم ممکن است خطا کند. پژوهشگران مستقل هنوز فرصت بررسی این مجموعه را نداشته‌اند، بنابراین ارقام فعلاً روایت خود شرکت است.