https://formal.land/blog/2024/12/20/translation-of-circom-to-coq

[giscus[bot]]

https://formal.land/blog/2024/12/20/translation-of-circom-to-coq

In this post, we present the beginning of our work to translate programs written in the Circom circuit language to the 🐓 Coq proof assistant. This work is part of our research on the formal verification of zero-knowledge systems.

https://formal.land/blog/2024/12/20/translation-of-circom-to-coq

[kmilesz]

Interesting! and what will be the difference compared to Veridise's Coda project?

[clarus]

Thanks for the link to Coda! As we understand, this is a circuit DSL that generates proof obligations in Coq as we want to do, but the Coda language is a different language from Circom. So, one would have to re-implement its circuits in Coda before doing the verification work and will have to maintain both, if we understand correctly. We aim to directly verify Circom programs.