الأمان والاختبار

Kontrol - formal verification tool based on Foundry and KEVM

تحقق شكلي

⁦Foundry⁩ · التعليم · حوكمة · تحقق شكلي · Solidity · التحقق في وقت التشغيل · نشر العقد · تحليل ثابت

التواصل الاجتماعي runtimeverification/kontrol(118 ☆)runtimeverification/optimism-ci(4 ☆)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆)runtimeverification/yearn-v3-term-vault(0 ☆)runtimeverification/Depeg-swap(0 ☆)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆)

يرفع ⁦Kontrol⁩ اختبارات خصائص ⁦Foundry⁩ إلى إثباتات مدعومة بـ ⁦KEVM⁩ بحيث يمكنك متابعة الضمانات الشكلية بعمل مواصفات مكتوبة بخط اليد أقل من ⁦KEVM⁩ الخام وحده.

موارد ذات صلة

K Semantics of the Ethereum Virtual Machine (EVM)

إن ⁦KEVM⁩ هي الدلالات القابلة للتنفيذ لإطار عمل ⁦K⁩ لـ ⁦EVM⁩: وجهها إلى رمز البايت عندما تحتاج إلى تنفيذ تم التحقق من توافقه، أو استكشاف رمزي، أو استنتاج الغاز، أو إثباتات تتتبع قواعد إيثيريوم عن كثب.

hax

إن ⁦hax⁩ هي أداة لترجمات عالية الضمان لمجموعة فرعية كبيرة من ⁦Rust⁩ إلى لغات رسمية مثل ⁦F*⁩ أو ⁦Rocq⁩.

Act

إن Act هي لغة المواصفات التصريحية وسلسلة الأدوات الخاصة بإيثيريوم لوصف جميع سلوكيات برنامج EVM بحيث يمكن لمحللات SMT، أو مثبتات النظريات، أو أدوات التحليل الاقتصادي التفكير في الصحة على مستوى رمز البايت وتوافق الحوافز، بما في ذلك إثباتات التحسين التلقائية مقابل التطبيقات الملموسة.

Verifereum

تربط ⁦Verifereum⁩ العقود الذكية لإيثيريوم بإثبات النظريات المدعوم بـ ⁦HOL4⁩ بحيث يمكنك استهداف ادعاءات صحة قوية جدًا عندما لا تكون مناهج ⁦SMT⁩ الآلية كافية.