The Cairo programming language and STARK technology provide an efficient means of recording computational results on blockchain. But how can we be sure that the results mean what we think they mean?

One thing we can do is write a mathematical proof that the algorithms and encodings are correct. An even better thing we can do is to have a computer check the mathematical proof, down to axiomatic primitives, to be certain that there are no errors. In this episode, we* describe the technology that enables us to do that, and we discuss the progress we have made towards verifying the Cairo toolchain.

We* - authors of A verified algebraic representation of Cairo program execution: Prof. Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer and Alon Titleman. 

In Mathematics We Trust