Nous avons vérifié la sécurité du protocole Fast Reed–Solomon Interactive Oracle Proof (FRI) - une pierre angulaire des preuves à divulgation nulle de connaissance de style STARK modernes et transparentes - en autoformalisant "Succinct Proofs and Linear Algebra" par Evans-Angeris avec Gauss.