يلتزم المزوّد أولاً بمعاملات النموذج ثم يرفق برهاناً حسابياً قابلاً للتحقق. ويتعلق الضمان بتنفيذ الحساب، ولا يثبت صحة المعلومات المولّدة.
وتظل الكلفة مرتفعة. وتقول أنثروبيك إن زمن حساب البرهان على وحدات معالجة الرسوميات بلغ نحو 70 إلى 95 ضعف زمن التشغيل المرجعي في اختبارها على نسخة مكمّمة من Llama 4 Maverick. وهذه قياسات الفريق، دون تحقق مستقل مثبت.
نُشرت الشيفرة والوثائق بترخيص Apache 2.0. وتوضح الوثائق أن البرامج لم تخضع لتدقيق أمني مستقل، وأن الضمانات الرسمية للمتحقق المكتوب بلغة Lean لا تشمل تلقائياً المتحقق السريع بلغة C++. ويظل العمل تقدماً بحثياً مرحلياً.