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

Certora Prover

تحقق شكلي

عرض على ⁦GitHub⁩ (يفتح في علامة تبويب جديدة)

عرض التالي

Kontrol - formal verification tool based on Foundry and KEVM

نبذة عن ⁦Certora Prover⁩

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.

الوسوم

  • تحقق شكلي
  • التحقق
  • الأمان

المستودعCertora

معلومات

النوع
تحقق شكلي
نجوم ⁦GitHub⁩
339
الترخيص
GPL-3.0
مراجعة الإدراج
سبتمبر 2026

أدوات مشابهة

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

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

hax

hax

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

Act

Act

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