EthSystems تأیید فرموله حوضچه حریم خصوصی را به پایان رساند و کد بایت Sepolia را پوشش داد

سازمان فناوری حریم خصوصی اتریوم EthSystems اعلام کرد که تأیید فرموله حوضچه حریم خصوصی خود را به پایان رسانده است، که دامنه آن از مشخصات مکتوب تا کد بایت در شبکه آزمایشی Sepolia را شامل می‌شود. در طول فرآیند تأیید، از ابزارهای مختلفی استفاده شده است؛ مدل‌ها، مدارها و هش‌ها با استفاده از Lean، قراردادها با Halmos و Kontrol، کیف پول‌ها با Aeneas و Verus، و تأییدکننده‌ها و استقرار از طریق بازسازی بایت به بایت بررسی شده‌اند. دو بار خرج کردن و حفظ ارزش توسط ماشین تئوری Lean تأیید شده است. در مجموع ۶ مشکل در تأیید شناسایی شد که ۳ مورد از آن‌ها در خود ابزار تأیید بود. تیم همچنین فرضیات وابسته‌ای را که هنوز به آن‌ها متکی هستند، شامل عدم برخورد هش، رد تأییدهای جعلی توسط تأییدکننده‌ها و سازگاری رفتار قرارداد با مدل، فهرست کرده است.