better.codes اتریوم امنیت ZK را به رقابتی با داوری ماشینی تبدیل می‌کند

تیم راستی‌آزمایی رسمی بنیاد اتریوم better.codes را راه‌اندازی کرده است؛ چالشی پژوهشی که یک پرسش بنیادی در فناوری دانش صفر را هدف می‌گیرد: چه مقدار از امنیت ادعاشده برای SNARKهای مبتنی بر هش واقعاً اثبات شده و چه مقدار هنوز بر حدس‌ها تکیه دارد؟

این چالش روی koalaIRS12 تمرکز دارد؛ مسئله‌ای دربارهٔ نزدیکی کدهای رید–سالومون که به ابتکار Proximity Prize مرتبط است و به‌صورت کامل در Lean و از طریق ArkLib صورت‌بندی شده است. شرکت‌کنندگان می‌توانند مدل‌های هوش مصنوعی، ابزارهای جست‌وجوی اثبات و محیط‌های راستی‌آزمایی خود را وارد کنند. هدف آن‌ها اثبات یک کران پایینِ بزرگ‌تر برای soundness، درون یک گزارهٔ قضیه و مجموعه‌پارامترهای ثابت، است.

این رویکرد نقش معمول هوش مصنوعی در رمزنگاری را تغییر می‌دهد. از یک عامل خواسته نمی‌شود صرفاً اثباتی چشمگیر تولید کند یا امتیازی بگیرد که به ارزیاب غیرشفاف وابسته باشد. هر ارسال ابتدا با گزارهٔ قضیهٔ تثبیت‌شده مقایسه می‌شود و سپس هستهٔ Lean آن را دوباره بررسی می‌کند. نتایج پذیرفته‌شده به مخزن عمومی منتقل می‌شوند و نام حل‌کننده و مدل هوش مصنوعی مورد استفاده نیز ثبت می‌شود.

این هدف از آن جهت مهم است که SNARKهای مبتنی بر هش در محیط تولید—از جمله سامانه‌های مورد استفاده در zk-rollupها و zkVMها—به شکاف‌های نزدیکی رید–سالومون و نتایج توافق هم‌بسته متکی هستند. بنیاد اتریوم می‌گوید سامانه‌های مستقر معمولاً امنیت ۱۲۸ بیتی را هدف می‌گیرند، اما کران‌های ریاضیِ فعلاً اثبات‌شده کاملاً به سطحی که پژوهشگران با این هدف مرتبط می‌دانند نمی‌رسند. بنابراین better.codes برای کاهش فاصلهٔ میان امنیت حدس‌زده‌شده و امنیت بررسی‌شده توسط ماشین طراحی شده است.

جزئیات مهندسی مهم، خط پایهٔ مشترک است. لم‌ها، روش‌های اثبات و نتایج ناممکن‌بودنِ حاصل از ارسال‌های پذیرفته‌شده در ادامه به مخزن اصلی بازگردانده می‌شوند تا شرکت‌کنندگان بعدی بتوانند روی آن‌ها کار کنند. در نتیجه، جدول رتبه‌بندی فقط عامل‌ها را مرتب نمی‌کند؛ هدفش این است که پیشرفت را انباشتی و قابل ممیزی کند.

گزارشی از تجربهٔ پروژهٔ راستی‌آزمایی zkEVM بنیاد اتریوم در ماه مه ۲۰۲۶ نشان می‌دهد چرا این شیوه عملی‌تر شده است. پژوهشگران ابزارهای استخراج Rust به Lean مانند Aeneas و Hax را با کتابخانه‌های رمزنگاری رسمی مانند ArkLib و CompPoly ترکیب کردند و سپس از اثبات‌گرهای هوش مصنوعی برای بستن برخی تعهدات در کد رمزنگاری Plonky3 و RISC Zero استفاده کردند. این مقاله تأکید می‌کند که هستهٔ Lean همهٔ اثبات‌ها را دوباره بررسی می‌کند، اما محدودیت‌های واقعی مانند اختلاف نسخهٔ ابزارها، مرزهای استخراج، لم‌های مفقود و نیاز به کار دستی را نیز ثبت می‌کند.

این تفاوت برای سازندگان ZK مهم است. better.codes همهٔ اثبات‌گرهای مستقر را تأیید نمی‌کند و صرفاً به‌دلیل تولید یک استدلال توسط هوش مصنوعی، آن را معتبر نمی‌سازد. این پروژه محیطی محدود و بازتولیدپذیر فراهم می‌کند که در آن فقط یک اثبات بررسی‌شده توسط هسته می‌تواند کران منتشرشده را بهبود دهد.

عدد ۱۲۸ بیت هدف چالش است، نه نتیجه‌ای که در زمان راه‌اندازی به‌دست آمده باشد. بنیاد همچنین می‌گوید شرایط مشارکت، ارزیابی، جوایز و پرداخت‌ها ممکن است در جریان توسعهٔ برنامه تغییر کنند. درس فوری برای توسعه‌دهندگان محدود اما مهم است: راستی‌آزمایی رسمی از ممیزی‌های منفرد به‌سوی زیرساخت اثبات عمومی و قابل استفادهٔ مجدد حرکت می‌کند و هوش مصنوعی درون این مرز اعتماد به‌عنوان دستیار جست‌وجوی اثبات آزمایش می‌شود، نه مرجع نهایی.