پروژهٔ StateSync-GKR دو مسیر را کنار هم پیش برده است: بررسی ماشینی تضمین‌های GKR و بهینه‌سازی یک sparse prover برای به‌روزرسانی sparse-Merkle. نویسندگان می‌گویند تا جایی که اطلاع دارند، این نخستین کران soundness برای GKR روی circuitهای لایه‌ای عمومی است که در Isabelle/HOL بررسی ماشینی شده است. نسخهٔ 1.2 نیز throughput تولید proof را بین ۲٫۴۱ تا ۲٫۷۱ برابر افزایش داده، در حالی که proofهای مقایسه‌شده بایت‌به‌بایت یکسان مانده‌اند.
در GKR، تنها ورودی و خروجی circuit موضوع commitment هستند، نه لایه‌های میانی. این روش با اجرای Sumcheck برای هر لایه، ادعای مربوط به خروجی را مرحله‌به‌مرحله به ادعایی دربارهٔ ورودی کاهش می‌دهد. کار جدید، circuitهایی با gateهای خطی، ضرب و توان سوم را پوشش می‌دهد. بررسی ماشینی روی بسط درجهٔ چهارِ field سی‌ویک‌بیتی KoalaBear نیز انجام شده؛ همان مختصاتی که پیاده‌سازی استفاده می‌کند.
تضمین ارائه‌شده فقط دربارهٔ محاسبات GKR نیست. پژوهش، ارتباط circuit با به‌روزرسانی sparse-Merkle را هم مدل می‌کند. بااین‌حال، همهٔ بخش‌ها وضعیت یکسانی ندارند: بخشی از نتایج در Isabelle/HOL بررسی شده‌اند و برخی، از جمله گزارهٔ امنیتی مربوط به هر ورودی با فرض درستی hash sub-circuitها، اثبات روی کاغذ دارند. همچنین node hash مبتنی بر Poseidon2 در این طراحی collision-resistant نیست؛ استدلال امنیتی به Position Binding درخت تکیه می‌کند.
اتصال مدل رسمی به Rust نیز هنوز کامل نیست. قراردادهای Creusot و اثبات‌های ثبت‌شدهٔ Why3 و SMT، تعدادی از تابع‌های compiler، موتور Sumcheck و رابط hash gadget را به مدل مرتبط می‌کنند. اما اثبات رابطهٔ صریح میان مقدارهای Rust و مدل برای verifier حاصل از compile، همچنان حلقهٔ باز این زنجیره است.
در اندازه‌گیری‌های اجرا، sparse prover در عرض ۴٬۰۹۶ حدود ۸۹ برابر حافظهٔ اوج کمتری از مرجع dense مخصوص آزمایش مصرف کرده است. در نسخهٔ 1.2، hash هر ۱۳٬۸۲۴ proof مقایسه‌شده بدون تغییر مانده و نظریه‌های Isabelle نیز دست‌نخورده‌اند. روی یک VM با ۱۹۲ هسته و بار هزار درخواست در ثانیه، p99 زمان رسیدن به پذیرش تأییدشده از ۴۴۰ میلی‌ثانیه با مسیر جدید سرویس‌دهی به ۷۵ و با محاسبات جدید به ۳۴ میلی‌ثانیه رسیده است. این اعداد مقایسه با baselineهای خود StateSync-GKR هستند، نه سامانه‌های دیگر.
