وفقاً لـ ChainCatcher، نشر فيتاليك مقالاً بعنوان “A shallow dive into formal verification” اليوم، يناقش كيف يمكن للتحقق الصوري تعزيز كل من الأمان والكفاءة في تطوير إيثريوم. يمكن للمطورين استخدام Lean أو كود بايت EVM أو لغة التجميع لكتابة التعليمات البرمجية والتحقق من صحتها من خلال براهين رياضية قابلة للتحقق تلقائياً. أشار فيتاليك إلى أن التحقق الصوري مناسب بشكل خاص للأنظمة المعقدة مثل STARKs، وتوافق الإجماع القابل للتسامح مع الأعطال البيزنطية، وZK-EVM، والتواقيع ما بعد الكمية، رغم أنه يواجه قيوداً تشمل أخطاء في المواصفات، وتغطية غير مكتملة للشفرة، والهجمات على مستوى العتاد.
أخبار ذات صلة