نحن Runtime Verification، شركة بحث وتطوير تبني أدوات صارمة لضمان سلامة وصحة الأنظمة الحرجة. قام فريقنا بتطوير KEVM، وهي الدلالات الرسمية الأكثر اكتمالاً واختبارًا لآلة إيثريوم الافتراضية (EVM)، والمكتوبة في K Framework. إن KEVM ليس مجرد مواصفات، بل هو مواصفات قابلة للتنفيذ يمكن استخدامها للتفكير الرمزي حول العقود الذكية، وإجراء اختبارات المطابقة، وتحليل استخدام الغاز، وتصحيح أخطاء البرامج، والتحقق رسميًا من خصائص الصحة. يجتاز مجموعة اختبارات إيثريوم الكاملة ويُستخدم للتحقق من العقود عالية القيمة، بما في ذلك رموز ERC-20 في كل من Solidity و Vyper. قمنا مؤخرًا بتحديث الدلالات لدعم ترقية Pectra. يتم استخدام KEVM بنشاط بواسطة Kontrol - أداة التحقق الرسمية الخاصة بنا لـ Solidity، والتي يتم استخدامها بنشاط من قبل الفرق الرائدة في نظام EVM البيئي، بما في ذلك Optimism و Ethereum Foundation و Lido و Uniswap، بالإضافة إلى باحثي الأمن والمدققين عبر مجتمع إيثريوم الأوسع. نحن نحافظ بنشاط على هذا المستودع، ونساهم في تطور بروتوكول إيثريوم، ونتكامل مع أدوات المطورين مثل Foundry. من خلال KEVM، نحن ندفع حدود ما هو ممكن في البنية التحتية للعقود الذكية الآمنة والصحيحة بشكل يمكن إثباته.
