از زمان فورک Prague، درخواست‌های لایه اجرا برای خروج ولیدیتورها و برداشت‌های جزئی از طریق یک قرارداد 504 بایتی در آدرس مشخصی پردازش می‌شوند. این قرارداد به صورت دستی برای اسمبلر geas نوشته شده است. در پایان هر بلاک، پروتکل یک سیستم کال به این قرارداد انجام می‌دهد که برای اجماع بسیار حیاتی است. EIP-7002 بلاکی که سیستم کال آن شکست بخورد را نامعتبر می‌داند.
در Lean 4 دو ویژگی از بایت‌های runtime مستقر شده اثبات شده است: اولاً، سیستم کال همیشه موفق است، بدون توجه به محتوای ذخیره‌سازی قرارداد، و حداکثر 210,000 از 30,000,000 گاز اختصاص داده شده را مصرف می‌کند. ثانیاً، درخواست‌ها دقیقاً به ترتیب ورود پردازش می‌شوند. این ویژگی‌ها در برابر Jaune، یک semantics اجرایی از EVM و پردازش بلاک، بیان شده‌اند و فورک‌های Prague، Osaka، BPO1 و BPO2 را پوشش می‌دهند.
اثبات‌ها بدون استفاده از هیچ اصل اضافی به جز سه اصل استاندارد Lean انجام شده‌اند. قبل از deploy، قرارداد توسط چهار ممیزی و یک بررسی Halmos محدود به حلقه بررسی شده بود. نتایج اینجا بایت‌های مستقر شده را به پردازش بلاک Jaune متصل می‌کند و درخواست‌ها را از ارسال تا تحویل در طول تاریخچه‌ها دنبال می‌کند.
برای جزئیات بیشتر به منبع اصلی مراجعه کنید.
