A verified algebraic representation of cairo program execution. - Jeremy Avigad; Lior Goldberg; David Levit; Yoav Seginer; Alon Titelman (CPP, 2022)

A Proof-Producing Compiler for Blockchain Applications. - Jeremy Avigad; Lior Goldberg; David Levit; Yoav Seginer; Alon Titelman (J. Autom. Reason., 2025)