أعلنت EthSystems عن إتمام التحقق الصوري من مجمع الخصوصية، بدءًا من المواصفات المكتوبة وصولًا إلى الشيفرة الثنائية التي تعمل فعليًا على شبكة Sepolia التجريبية. جرى التحقق على مستويات مختلفة باستخدام أدوات متخصصة: Lean للنموذج والدارات ودوال التجزئة، وHalmos وKontrol للعقود، وAeneas وVerus للمحفظة، بينما جرى التحقق من المُدقِّق وعمليات النشر عبر إعادة البناء بايتًا ببايت.
اجتازت خاصيتا منع الإنفاق المزدوج والحفاظ على القيمة التحققَ الآلي بواسطة مبرهنات Lean. وكُشف عن 6 مشكلات خلال العملية، 3 منها في أدوات التحقق نفسها، لا في شيفرة البروتوكول.
كما أوضح الفريق الافتراضات التي لا يزال يعتمد عليها: مقاومة دوال التجزئة للتصادمات، ورفض المُدقِّق للأدلة المزيفة، وتطابق سلوك العقد مع النموذج. وهنا تقف حدود ما يمكن أن يشمله التحقق الصوري؛ فالافتراضات الخارجة عن النموذج لم تدخل في البرهان.
#ETH
اجتازت خاصيتا منع الإنفاق المزدوج والحفاظ على القيمة التحققَ الآلي بواسطة مبرهنات Lean. وكُشف عن 6 مشكلات خلال العملية، 3 منها في أدوات التحقق نفسها، لا في شيفرة البروتوكول.
كما أوضح الفريق الافتراضات التي لا يزال يعتمد عليها: مقاومة دوال التجزئة للتصادمات، ورفض المُدقِّق للأدلة المزيفة، وتطابق سلوك العقد مع النموذج. وهنا تقف حدود ما يمكن أن يشمله التحقق الصوري؛ فالافتراضات الخارجة عن النموذج لم تدخل في البرهان.
#ETH
