أعلنت مجموعة بحثية من Ethereum Protocol Fellowship وInvisible Garden عن إحراز تقدم جديد في مشروع Etheorem، وفقًا لمنشور على منتدى Ethresearch. ووفقًا لـ Foresight News، يهدف المشروع إلى بناء مواصفة توافق لإيثريوم قابلة للتنفيذ بالكامل في Lean 4، باستخدام التحقق الرياضي الرسمي بدلًا من الاختبارات التقليدية للشفرة، وذلك لتقليل أخطاء المنطق ومنع الانقسامات (chain splits) الناتجة عن اختلافات التنفيذ.

أحرزت المواصفة نجاحًا في اجتياز جميع متجهات الاختبار لإصدارات مستقبلية ثلاثية للانقسام الصعب (hard fork) وهي Fulu وGloas، بما في ذلك آلية ePBS، وHeze، مع تغطية مجالات أساسية مثل انتقالات الحالة واختيار الفرع. تم التحقق من جميع المنطق بشكل مستقل عبر نواة Lean، ويهدف المشروع إلى توفير إطار تحقق عالي الأمان للترقيات المستقبلية لبروتوكول إيثريوم.