Hemos verificado la seguridad del protocolo Fast Reed–Solomon Interactive Oracle Proof (FRI) —una piedra angular de las demostraciones modernas de conocimiento cero transparentes al estilo STARK— autoformalizando "Succinct Proofs and Linear Algebra" de Evans-Angeris con Gauss.