تخطي إلى المحتوى الرئيسي
الأمان والاختبار

hax

تحقق شكلي

زيارة الموقع الإلكتروني (يفتح في علامة تبويب جديدة)⁦hax⁩ على ⁦GitHub⁩ (يفتح في علامة تبويب جديدة)

عرض التالي

Certora Prover

نبذة عن ⁦hax⁩

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

الوسوم

  • تحقق شكلي

المستودعcryspen

معلومات

النوع
تحقق شكلي
نجوم ⁦GitHub⁩
502
الترخيص
Apache-2.0
مراجعة الإدراج
يوليو 2026

أدوات مشابهة

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

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

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

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

Act

Act

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