我們已經驗證了快速里德-所羅門互動Oracle證明（FRI）協議的安全性——這是現代透明的STARK風格零知識證明的基石——通過自動形式化Evans-Angeris的《簡潔證明與線性代數》與高斯。