This is where the formalization work related to OSL lives. This is a work in progress. The goal is to create a formally verified arithmetic circuit compiler for zero knowledge proving and verification. Soundness (the inability to prove false statements) cannot effectively be tested; it can only be proven.
polytopoi / coq-arithmetization Goto Github PK
View Code? Open in Web Editor NEWThis project forked from orbis-tertius/coq-arithmetization
Coq formalization of Sigma^1_1 arithmetization (WIP)
License: Apache License 2.0