{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T18:43:27Z","timestamp":1773341007781,"version":"3.50.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62572294"],"award-info":[{"award-number":["62572294"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    <jats:italic toggle=\"yes\">Zero-knowledge proof (ZKP)<\/jats:italic>\n                    systems have surged attention and held a fundamental role in contemporary cryptography.\n                    <jats:italic toggle=\"yes\">Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK)<\/jats:italic>\n                    protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This article introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the\n                    <jats:italic toggle=\"yes\">computer algebra system<\/jats:italic>\n                    . The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC\n                    <jats:sup>4<\/jats:sup>\n                    , is proposed to represent the implementation of the method. Experiments show that AC\n                    <jats:sup>4<\/jats:sup>\n                    demonstrates an increase in the solved rate, showing a 36.7% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.\n                  <\/jats:p>","DOI":"10.1145\/3786607","type":"journal-article","created":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T21:14:48Z","timestamp":1769030088000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["AC4: Algebraic Computation Checker for Circuit Constraints in Zero-Knowledge Proofs"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9010-5364","authenticated-orcid":false,"given":"Qizhe","family":"Yang","sequence":"first","affiliation":[{"name":"Shanghai Normal University","place":["Shanghai, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1445-195X","authenticated-orcid":false,"given":"Boxuan","family":"Liang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University","place":["Shanghai, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3675-1344","authenticated-orcid":false,"given":"Hao","family":"Chen","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University","place":["Shanghai, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-7112","authenticated-orcid":false,"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science, Shanghai Jiao Tong University","place":["Shanghai, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,12]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","unstructured":"John Abbott and Anna Maria Bigatti. 2007. CoCoALib: a C++ library for doing Computations in Commutative Algebra. Retrieved from https:\/\/cocoa.dima.unige.it\/cocoa\/cocoalib","DOI":"10.1145\/1358190.1358204"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15497-3_10"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.aam.2006.08.008"},{"key":"e_1_3_2_5_2","unstructured":"Aztec. 2022. Disclosure of Recent Vulnerabilities. Retrieved from https:\/\/hackmd.io\/@aztec-network\/disclosure-of-recent-vulnerabilities"},{"key":"e_1_3_2_6_2","article-title":"Formalizing Soundness Proofs of SNARKs","author":"Bailey Bolton","year":"2023","unstructured":"Bolton Bailey and Andrew Miller. 2023. Formalizing Soundness Proofs of SNARKs. Cryptology ePrint Archive, Paper 2023\/656. Retrieved from https:\/\/eprint.iacr.org\/2023\/656","journal-title":"Cryptology ePrint Archive, Paper 2023\/656"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16441-5_5"},{"key":"e_1_3_2_8_2","article-title":"Automatic Generation of Sound Zero-Knowledge Protocols","author":"Bangerter Endre","year":"2008","unstructured":"Endre Bangerter, Jan Camenisch, Stephan Krenn, Ahmad-Reza Sadeghi, and Thomas Schneider. 2008. Automatic Generation of Sound Zero-Knowledge Protocols. Cryptology ePrint Archive, Paper 2008\/471. Retrieved from https:\/\/eprint.iacr.org\/2008\/471","journal-title":"Cryptology ePrint Archive, Paper 2008\/471"},{"key":"e_1_3_2_9_2","first-page":"12","article-title":"On the design and implementation of efficient zero-knowledge proofs of knowledge","volume":"9","author":"Bangerter Endre","year":"2009","unstructured":"Endre Bangerter, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider, and Joe-Kai Tsay. 2009. On the design and implementation of efficient zero-knowledge proofs of knowledge. Software Performance Enhancements for Encryption and Decryption and Cryptographic Compilers\u2013SPEED-CC 9 (2009), 12\u201313.","journal-title":"Software Performance Enhancements for Encryption and Decryption and Cryptographic Compilers\u2013SPEED-CC"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3232813"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-34799-2_4"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.36"},{"key":"e_1_3_2_13_2","first-page":"781","volume-title":"Proceedings of the 23rd USENIX Security Symposium (USENIX Security 14)","author":"Ben-Sasson Eli","year":"2014","unstructured":"Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer, and Madars Virza. 2014. Succinct non-interactive zero knowledge for a von neumann architecture. In Proceedings of the 23rd USENIX Security Symposium (USENIX Security 14). USENIX Association, San Diego, CA, 781\u2013796. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity14\/technical-sessions\/presentation\/ben-sasson"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62222"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/3370272.3370309"},{"key":"e_1_3_2_17_2","unstructured":"Richard B. Kreckel Bruno Haible. 2004. CLN - Class Library for Numbers. Retrieved from https:\/\/www.ginac.de\/CLN\/"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2005.09.007"},{"key":"e_1_3_2_19_2","unstructured":"Tornado Cash. 2019. Tornado.Cash Got Hacked. By Us. Retrieved from https:\/\/tornado-cash.medium.com\/tornado-cash-got-hacked-by-us-b1e012a3c9a8"},{"key":"e_1_3_2_20_2","article-title":"Compositional Formal Verification of Zero-Knowledge Circuits","author":"Coglio Alessandro","year":"2023","unstructured":"Alessandro Coglio, Eric McCarthy, Eric Smith, Collin Chin, Pranav Gaddamadugu, and Michel Dellepere. 2023. Compositional Formal Verification of Zero-Knowledge Circuits. Cryptology ePrint Archive, Paper 2023\/1278. Retrieved from https:\/\/eprint.iacr.org\/2023\/1278","journal-title":"Cryptology ePrint Archive, Paper 2023\/1278"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.393.9"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07407-4_17"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/780506.780516"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00005-5"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.26"},{"key":"e_1_3_2_27_2","article-title":"PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive Arguments of Knowledge","author":"Gabizon Ariel","year":"2019","unstructured":"Ariel Gabizon, Zachary J. Williamson, and Oana Ciobotaru. 2019. PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive Arguments of Knowledge. Cryptology ePrint Archive, Paper 2019\/953. Retrieved from https:\/\/eprint.iacr.org\/2019\/953","journal-title":"Cryptology ePrint Archive, Paper 2019\/953"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22178"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46803-6_9"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63498-7_23"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.29007\/4n6w"},{"key":"e_1_3_2_32_2","unstructured":"Fatemeh Heidari. 2023. halo2-analyzer. Retrieved from https:\/\/github.com\/quantstamp\/halo2-analyzer"},{"key":"e_1_3_2_33_2","unstructured":"Iden3. 2022. Circomlib: Library of Basic Circuits for Circom. Retrieved from https:\/\/github.com\/iden3\/circomlib"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48184-2_4"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00133"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_3_2_37_2","unstructured":"Numen Cyber Labs. 2023. Security Concerns for Zero-Knowledge Proofs in Blockchain: A Comprehensive Guide by Numen Cyber."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_39_2","article-title":"Certifying Zero-Knowledge Circuits with Refinement Types","author":"Liu Junrui","year":"2023","unstructured":"Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, I\u015f\u0131l Dillig, and Yu Feng. 2023. Certifying Zero-Knowledge Circuits with Refinement Types. Cryptology ePrint Archive, Paper 2023\/547. Retrieved from https:\/\/eprint.iacr.org\/2023\/547","journal-title":"Cryptology ePrint Archive, Paper 2023\/547"},{"key":"e_1_3_2_40_2","unstructured":"Anton Lucian. 2019. Zcash Denial-Of-Service Attack Costs Just $2.89 per Day - BeInCrypto. Retrieved from https:\/\/beincrypto.com\/zcash-denial-of-service-attack-costs-just-2-89-per-day\/"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2012.102"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2011.6113989"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_44_2","unstructured":"Tails of Bits. 2023. Circomspect. Retrieved from https:\/\/github.com\/trailofbits\/circomspect"},{"key":"e_1_3_2_45_2","article-title":"Satisfiability Modulo Finite Fields","author":"Ozdemir Alex","year":"2023","unstructured":"Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and Clark Barrett. 2023. Satisfiability Modulo Finite Fields. Cryptology ePrint Archive, Paper 2023\/091. Retrieved from https:\/\/eprint.iacr.org\/2023\/091","journal-title":"Cryptology ePrint Archive, Paper 2023\/091"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_1"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_8"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591282"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2856449"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03338-8"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218721"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/PRDC59308.2023.00031"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.31980\/mosharafa.v12i1.748"},{"key":"e_1_3_2_54_2","article-title":"Automated Analysis of Halo2 Circuits","author":"Soureshjani Fatemeh Heidari","year":"2023","unstructured":"Fatemeh Heidari Soureshjani, Mathias Hall-Andersen, MohammadMahdi Jahanara, Jeffrey Kam, Jan Gorzny, and Mohsen Ahmadvand. 2023. Automated Analysis of Halo2 Circuits. Cryptology ePrint Archive, Paper 2023\/1051. Retrieved from https:\/\/eprint.iacr.org\/2023\/1051","journal-title":"Cryptology ePrint Archive, Paper 2023\/1051"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833732"},{"issue":"10","key":"e_1_3_2_56_2","first-page":"1199","article-title":"What is \u2026 a grobner basis?","volume":"52","author":"Sturmfels Bernd","year":"2005","unstructured":"Bernd Sturmfels. 2005. What is \u2026 a grobner basis? Notices-American Mathematical Society 52, 10 (2005), 1199.","journal-title":"Notices-American Mathematical Society"},{"key":"e_1_3_2_57_2","series-title":"Proceedings of Machine Learning Research","first-page":"1540","volume-title":"Proceedings of the 29th Annual Conference on Learning Theory.","volume":"49","author":"Volkovich Ilya","year":"2016","unstructured":"Ilya Volkovich. 2016. A guide to learning arithmetic circuits. In Proceedings of the 29th Annual Conference on Learning Theory.Vitaly Feldman, Alexander Rakhlin, and Ohad Shamir (Eds.), Proceedings of Machine Learning Research, Vol. 49, PMLR, Columbia University, New York, New York, USA, 1540\u20131561. Retrieved from https:\/\/proceedings.mlr.press\/v49\/volkovich16.html"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2007.4601876"},{"key":"e_1_3_2_59_2","article-title":"Practical Security Analysis of Zero-Knowledge Proof Circuits","author":"Wen Hongbo","year":"2023","unstructured":"Hongbo Wen, Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Isil Dillig, and Yu Feng. 2023. Practical Security Analysis of Zero-Knowledge Proof Circuits. Cryptology ePrint Archive, Paper 2023\/190. Retrieved from https:\/\/eprint.iacr.org\/2023\/190","journal-title":"Cryptology ePrint Archive, Paper 2023\/190"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1155\/2014\/560484"},{"key":"e_1_3_2_61_2","article-title":"The halo2 Book","unstructured":"zcash. [n. d.]. The halo2 Book. Retrieved from https:\/\/zcash.github.io\/halo2\/index.html. [Online: The halo2 Book].","journal-title":"R"},{"key":"e_1_3_2_62_2","unstructured":"Zcash. 2023. Zcash: Privacy-protecting digital currency. Retrieved from https:\/\/z.cash\/"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3786607","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T09:05:50Z","timestamp":1773306350000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3786607"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,12]]},"references-count":61,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3786607"],"URL":"https:\/\/doi.org\/10.1145\/3786607","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,12]]},"assertion":[{"value":"2025-06-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-21","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}