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
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|