arxiv: 2605.15163 · v1 · submitted 2026-05-14 · 💻 cs.LO

Recognition: 2 theorem links

· Lean Theorem

Automating Bitvector and Finite Field Equivalence Proofs in Lean

Elizaveta Pertseva , Valentin Robert , Clark Barrett , James Parker

Authors on Pith no claims yet

Pith reviewed 2026-05-15 02:46 UTC · model grok-4.3

classification 💻 cs.LO

keywords Leantacticbitvectorfinite fieldzero-knowledge proofequivalence proofrange lemmabit-blasting

0 comments

The pith

Lean tactic automates finite field to bitvector translations and solves 19% more ZKP benchmarks than SMT solvers

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a tactic in Lean called BitModEq to automate proofs of equivalence between bitvector and finite field operations in quantifier-free statements. Existing approaches to verifying zero-knowledge proof circuits either require manual proofs or rely on SMT solvers that scale poorly due to difficulties with conversion operators and inequalities. The tactic uses range lemmas and case analysis to create verified translations from finite fields to bitvectors that can then be bit-blasted. Combined with bit-blasting, the method solves 19% more ZKP arithmetization benchmarks than state-of-the-art SMT solvers.

Core claim

The BitModEq tactic leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. This enables automated proofs for quantifier-free statements mixing bitvector and finite field operations. When paired with bit-blasting, the tactic outperforms state-of-the-art SMT solvers by solving 19% more ZKP arithmetization benchmarks.

What carries the argument

BitModEq tactic that applies range lemmas and case analysis to produce verified translations from finite fields to bitvectors

If this is right

More zero-knowledge proof circuit encodings can be verified automatically.
Verification workflows gain scalability for statements involving both bitvectors and finite fields.
Bit-blasting becomes applicable after the automated translation step.
Reliance on manual proofs or direct SMT solving decreases for these mixed arithmetic problems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The tactic may extend to other interactive theorem provers for similar arithmetic translation tasks.
Hybrid verification systems could use this tactic as a preprocessing step before calling SMT solvers.
The approach could support verification of additional cryptographic protocols that rely on modular arithmetic conversions.

Load-bearing premise

The range lemmas and case analysis in BitModEq produce sound translations for all relevant cases in ZKP arithmetization without missing edge cases or introducing incorrect equivalences.

What would settle it

A specific ZKP arithmetization benchmark where BitModEq fails to produce a correct verified translation that a manual proof or SMT solver can handle.

Figures

Figures reproduced from arXiv: 2605.15163 by Clark Barrett, Elizaveta Pertseva, James Parker, Valentin Robert.

**Figure 1.** Figure 1: BitModEq workflow. The tactic accepts terms over ΣFP and ΣBV, and terms originating from toNat and bvToNat operators. It first converts FP terms to N terms and then converts N terms to BVN terms. Inequalities are discharged by rng_analyze. If rng_analyze cannot prove an inequality from the original goal, the tactic returns unknown; if it cannot prove a premise from a translation rule, a different rule is a… view at source ↗

**Figure 2.** Figure 2: Translation rules from FP to N. Γ = {G, H} denotes the proof context, where G is the set of goals and H is the global set of shared hypotheses. Finite Fields to Natural Numbers mvZModSub groups additions before subtractions to accumulate positive values and ensure minimal underflow cases. injNat replaces finite field equations with natural number equations. distNat distributes the toNat operator over addi… view at source ↗

**Figure 3.** Figure 3: Translation rules from N to BVN . While the majority of ZKP arithmetizations only use finite field variables to represent bits, the restriction that a variable must be 0 or 1 relies on finite field reasoning (finite fields’ not having zero divisors), because finite fields do not naturally support comparisons or the Boolean operator or. Thus, we add sqrBds to detect bit encodings and translate them to natur… view at source ↗

**Figure 4.** Figure 4: Strategies for applying translation rules from Figures [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗

**Figure 5.** Figure 5: Range analysis rules for inequality decomposition. We use [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗

**Figure 6.** Figure 6: Range analysis rules for placeholder variable elimination. Notation follows [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗

**Figure 7.** Figure 7: Range analysis rules for constant and bit reasoning. Notation follows that [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗

**Figure 8.** Figure 8: Cactus plots across benchmark suites comparing [PITH_FULL_IMAGE:figures/full_fig_p016_8.png] view at source ↗

read the original abstract

Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

BitModEq gives a Lean tactic for field-to-bitvector translations that beats SMT by 19% on ZKP benchmarks, but the soundness of its range lemmas needs checking.

read the letter

The paper introduces BitModEq, a Lean tactic that uses range lemmas and case analysis to automate verified translations from finite field operations to bitvectors. When combined with bit-blasting, it reportedly solves 19% more ZKP arithmetization benchmarks than current SMT solvers. This targets a practical bottleneck where SMT tools struggle with conversion operators and inequality reasoning in zero-knowledge proof circuit encodings. The tactic produces Lean-checked translations, which is a clear step up from manual proofs or unverified external solvers for this class of quantifier-free statements. The work is grounded in an existing formal system and focuses on a real pain point for people verifying cryptographic circuits. The 19% improvement is presented as an empirical result against external SMT baselines, which avoids circularity. That said, the description leaves open whether the range lemmas fully cover bitwidth alignments and modular reduction cases that commonly appear in ZKP arithmetization. If those lemmas miss edge cases, the tactic could either fail to terminate on valid inputs or accept incorrect equivalences, which would make the benchmark comparison unreliable. Benchmark selection and error-handling details are also thin, so the performance claim is hard to assess without more data. This paper is aimed at researchers doing interactive theorem proving for cryptography, especially those already working in Lean. Readers who need tactics for bitvector reasoning in circuit verification would get concrete ideas from it. It deserves peer review because the core tactic is implemented and tested, even if the soundness argument and experimental setup need tightening.

Referee Report

2 major / 2 minor

Summary. The paper introduces a Lean tactic BitModEq that employs range lemmas and case analysis to generate verified translations from finite-field to bitvector representations, enabling automation of quantifier-free equivalence proofs that mix both domains. When combined with bit-blasting, the tactic is reported to solve 19% more ZKP arithmetization benchmarks than state-of-the-art SMT solvers.

Significance. If the soundness of the translations holds, the work would provide a practical advance in mechanized verification of zero-knowledge proof circuits by mitigating known SMT weaknesses with conversion operators and inequalities. The empirical benchmark improvement and the use of a verified tactic in Lean constitute a concrete contribution to the intersection of formal methods and cryptographic verification.

major comments (2)

[BitModEq tactic and range lemmas] The central performance claim rests on BitModEq producing sound translations, yet the manuscript provides no machine-checked proof or exhaustive case analysis establishing that the range lemmas and case splits cover all alignments between bitvector widths and field moduli (including modular reduction cases typical in ZKP arithmetization). This directly affects the validity of the SMT comparison.
[Experimental evaluation] Benchmark results are presented without details on selection criteria, total number of instances, timeout settings, or how soundness of the tactic was validated on the solved instances; the 19% figure therefore lacks the supporting data needed to assess reproducibility and robustness.

minor comments (2)

[Introduction] The abstract and introduction use the term 'verified translations' without an early pointer to the precise statement of soundness that is later proved (or not) for BitModEq.
[Evaluation tables] Figure captions for the benchmark tables could explicitly state the SMT solvers and versions used for the baseline comparison.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive comments, which highlight important aspects of soundness and reproducibility. We address each major comment below and will make revisions to strengthen the manuscript accordingly.

read point-by-point responses

Referee: [BitModEq tactic and range lemmas] The central performance claim rests on BitModEq producing sound translations, yet the manuscript provides no machine-checked proof or exhaustive case analysis establishing that the range lemmas and case splits cover all alignments between bitvector widths and field moduli (including modular reduction cases typical in ZKP arithmetization). This directly affects the validity of the SMT comparison.

Authors: The BitModEq tactic is fully implemented in Lean, and its soundness is machine-checked by the Lean kernel through the definitions of the range lemmas and the case analysis procedure. The manuscript describes the approach but does not include the full formal proof details to keep the presentation accessible. We will add a new subsection or appendix that outlines the key range lemmas, provides the structure of the case splits, and explains coverage for modular reduction cases common in ZKP arithmetization. This will make the soundness argument explicit while referencing the verified Lean code. revision: yes
Referee: [Experimental evaluation] Benchmark results are presented without details on selection criteria, total number of instances, timeout settings, or how soundness of the tactic was validated on the solved instances; the 19% figure therefore lacks the supporting data needed to assess reproducibility and robustness.

Authors: We agree that additional experimental details are necessary for full reproducibility. In the revised manuscript, we will expand the evaluation section to specify: the total number of benchmark instances (drawn from standard ZKP arithmetization suites), the selection criteria (including how instances mixing bitvector and finite field operations were chosen), the timeout settings used for both our tactic and the SMT solvers (e.g., 300 seconds per instance), and the validation procedure for soundness (cross-verification with manual Lean proofs on a subset and consistency checks with SMT results on solved cases). The 19% improvement is computed as the percentage increase in the number of solved instances relative to the best SMT solver baseline. revision: yes

Circularity Check

0 steps flagged

No circularity: tactic soundness and benchmark gains rest on external Lean verification and SMT comparisons

full rationale

The paper introduces the BitModEq tactic in Lean that applies range lemmas and case splits to produce verified finite-field-to-bitvector translations, then combines it with bit-blasting for ZKP benchmarks. The performance claim (19% more solved instances) is measured against external state-of-the-art SMT solvers on a fixed benchmark set; no parameter is fitted to the target result and then re-used as a prediction. No self-citation is invoked to justify uniqueness or to close the soundness argument; the formal guarantees are supplied directly by Lean’s kernel. The derivation therefore remains independent of its own outputs and does not reduce to any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The contribution is a new tactic implementation; no free parameters, additional axioms, or invented entities are introduced beyond standard Lean libraries for bitvectors and finite fields.

pith-pipeline@v0.9.0 · 5407 in / 937 out tokens · 42989 ms · 2026-05-15T02:46:54.417972+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat recovery theorem unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages

[1]

Isa semantics for armv8-a, risc-v, and cheri-mips.Proceedings of the ACM on Programming Languages, 3(POPL): 1–31, 2019

Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E Gray, Robert M Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, et al. Isa semantics for armv8-a, risc-v, and cheri-mips.Proceedings of the ACM on Programming Languages, 3(POPL): 1–31, 2019

work page 2019
[2]

Jolt: Snarks for virtual machines via lookups

Arasu Arun, Srinath Setty, and Justin Thaler. Jolt: Snarks for virtual machines via lookups. InAnnual International Conference on the Theory and Applications of Cryptographic Techniques, pages 3–33. Springer, 2024

work page 2024
[3]

A verified algebraic representation of cairo program execution

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titel- man. A verified algebraic representation of cairo program execution. In Proceedings of the 11th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs, pages 153–165, 2022

work page 2022
[4]

Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, YingSheng,CesareTinelli,andYoniZohar. cvc5:Aversatileandindustrial- strength SMT solver. InTACAS, 2022

work page 2022
[5]

Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kre- mer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Math- ias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zohar. Gen- erating and exploiting automated reasoning proof certificates.Commu- nications of the Association for Computing Machinery (CACM), 66(10): 86–95, Octo...

work page doi:10.1145/3587692 2023
[6]

Satisfiability modulo theories

Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. InHand- book of model checking, pages 305–343. Springer, 2018

work page 2018
[7]

Faest: algorithm specifications

Carsten Baum, Lennart Braun, Cyprien Delpech de Saint Guilhem, Michael Klooß, Christian Majenz, Shibam Mukherjee, Sebastian Ramacher, Chris- tian Rechberger, Emmanuela Orsini, Lawrence Roy, et al. Faest: algorithm specifications. Technical report, Technical report, National Institute of Standards and Technology, 2023

work page 2023
[8]

Interactive bitvector reasoning using verified bit-blasting

Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett, et al. Interactive bitvector reasoning using verified bit-blasting. Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3259– 3285, 2025

work page 2025
[9]

Towards fuzzing zero-knowledge proof circuits (short paper)

Stefanos Chaliasos, Imam Al-Fath, and Alastair Donaldson. Towards fuzzing zero-knowledge proof circuits (short paper). InProceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 98–104, 2025

work page 2025
[10]

Cheesecloth:{Zero-Knowledge}proofs of real world vulnerabilities

Santiago Cuéllar, Bill Harris, James Parker, Stuart Pernsteiner, and Eran Tromer. Cheesecloth:{Zero-Knowledge}proofs of real world vulnerabilities. 22 E. Pertseva et al. In32nd USENIX Security Symposium (USENIX Security 23), pages 6525– 6540, 2023

work page 2023
[11]

Cheesecloth: Zero-knowledge proofs of real- world vulnerabilities.ACM Transactions on Privacy and Security, 28(4): 1–35, 2025

Santiago Cuéllar Gempeler, Bill Harris, James Parker, Stuart Pernsteiner, Ian Sweet, and Eran Tromer. Cheesecloth: Zero-knowledge proofs of real- world vulnerabilities.ACM Transactions on Privacy and Security, 28(4): 1–35, 2025

work page 2025
[12]

Veritas: Verifying image trans- formations at scale

Trisha Datta, Binyi Chen, and Dan Boneh. Veritas: Verifying image trans- formations at scale. In2025 IEEE Symposium on Security and Privacy (SP), pages 4606–4623. IEEE, 2025

work page 2025
[13]

Wiley Hoboken, 2004

David Steven Dummit and Richard M Foote.Abstract algebra, volume 3. Wiley Hoboken, 2004

work page 2004
[14]

Elsevier, 2001

Herbert B Enderton.A mathematical introduction to logic. Elsevier, 2001

work page 2001
[15]

An smt-lib theory of finite fields

Thomas Hader and Alex Ozdemir. An smt-lib theory of finite fields. 2024

work page 2024
[16]

Interval arithmetic: From principles to implementation.Journal of the ACM (JACM), 48(5): 1038–1068, 2001

Timothy Hickey, Qun Ju, and Maarten H Van Emden. Interval arithmetic: From principles to implementation.Journal of the ACM (JACM), 48(5): 1038–1068, 2001

work page 2001
[17]

Zcash protocol specification.GitHub: San Francisco, CA, USA, 4(220):32, 2016

Daira Hopwood, Sean Bowe, Taylor Hornby, Nathan Wilcox, et al. Zcash protocol specification.GitHub: San Francisco, CA, USA, 4(220):32, 2016

work page 2016
[18]

Scalable verifi- cation of zero-knowledge protocols

Miguel Isabel, Clara Rodriguez-Nunez, and Albert Rubio. Scalable verifi- cation of zero-knowledge protocols. In2024 IEEE Symposium on Security and Privacy (SP), pages 1794–1812. IEEE, 2024

work page 2024
[19]

Verifying jolt zkvm lookup semantics

Carl Kwan, Quang Dao, and Justin Thaler. Verifying jolt zkvm lookup semantics. InInternational Conference on Financial Cryptography and Data Security, pages 163–179. Springer, 2025

work page 2025
[20]

Certifying zero- knowledge circuits with refinement types

Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Işıl Dillig, and Yu Feng. Certifying zero- knowledge circuits with refinement types. In2024 IEEE Symposium on Security and Privacy (SP), pages 1741–1759. IEEE, 2024

work page 2024
[21]

URLhttps://dl.acm.org/doi/10.1145/3372885.3373827

The mathlib Community. The lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367–381, New York, NY, USA, 2020. Associa- tion for Computing Machinery. ISBN 9781450370974.https://doi.org/ 10.1145/3372885.3373824. URLhttps://doi.org/10.1145/3372885. 3373824

work page doi:10.1145/3372885.3373824 2020
[22]

Springer Science & Business Media, 2012

Robert J McEliece.Finite fields for computer scientists and engineers, volume 23. Springer Science & Business Media, 2012

work page 2012
[23]

Secure and privacy-preserving voting system using zero- knowledge proofs.Applied and Computational Engineering, 8(1):328–333, 2023

Yizhuo Miao. Secure and privacy-preserving voting system using zero- knowledge proofs.Applied and Computational Engineering, 8(1):328–333, 2023

work page 2023
[24]

Lean- smt: An smt tactic for discharging proof goals in lean

Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. Lean- smt: An smt tactic for discharging proof goals in lean. InInternational Conference on Computer Aided Verification, pages 197–212. Springer, 2025

work page 2025
[25]

The lean 4 theorem prover and programming language

Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Automating Bitvector and Finite Field Equivalence Proofs in Lean 23 Event, July 12–15, 2021, Proceedings, page 625–635, Berlin, Heidel- berg, 2021. Springer-Verlag. ISBN...

work page doi:10.1007/978-3-030-79876-5_37 2021
[26]

Simplification by cooperating decision procedures.ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245–257, 1979

Greg Nelson and Derek C Oppen. Simplification by cooperating decision procedures.ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245–257, 1979

work page 1979
[27]

CirC: Compiler infras- tructure for proof systems, software verification, and more

Alex Ozdemir, Fraser Brown, and Riad S Wahby. CirC: Compiler infras- tructure for proof systems, software verification, and more. InIEEE S&P, 2022

work page 2022
[28]

Satisfia- bility modulo finite fields

Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and Clark Barrett. Satisfia- bility modulo finite fields. InCAV, 2023

work page 2023
[29]

Split gröbner bases for satisfiability modulo finite fields

Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett, and Işil Dillig. Split gröbner bases for satisfiability modulo finite fields. In CAV, 2024

work page 2024
[30]

Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs

Alex Ozdemir, Riad S Wahby, Fraser Brown, and Clark Barrett. Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs. Formal Methods in System Design, pages 1–28, 2025

work page 2025
[31]

Automated detection of under-constrained circuits in zero-knowledge proofs.Proceedings of the ACM on Programming Languages,7(PLDI):1510– 1532, 2023

Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, and Işıl Dil- lig. Automated detection of under-constrained circuits in zero-knowledge proofs.Proceedings of the ACM on Programming Languages,7(PLDI):1510– 1532, 2023

work page 2023
[32]

Integer reasoning modulo different constants in smt

Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Işil Dillig, and Clark Barrett. Integer reasoning modulo different constants in smt. InInternational Conference on Computer Aided Verification, pages 339–362. Springer, 2025

work page 2025
[33]

SMT fixed size bit-vectors theory.https://smtlib.cs.uiowa.edu/ theories-FixedSizeBitVectors.shtml, 2017

Silvio Ranise, Cesare Tinelli, and Clark Barrett. SMT fixed size bit-vectors theory.https://smtlib.cs.uiowa.edu/ theories-FixedSizeBitVectors.shtml, 2017

work page 2017
[34]

Twist and shout: Faster memory check- ing arguments via one-hot addressing and increments

Srinath Setty and Justin Thaler. Twist and shout: Faster memory check- ing arguments via one-hot addressing and increments. Cryptology ePrint Archive, Paper 2025/105, 2025. URLhttps://eprint.iacr.org/2025/ 105

work page 2025
[35]

Unlocking the lookup sin- gularity with lasso

Srinath Setty, Justin Thaler, and Riad Wahby. Unlocking the lookup sin- gularity with lasso. InAnnual International Conference on the Theory and Applications of Cryptographic Techniques, pages 180–209. Springer, 2024

work page 2024
[36]

Reasoning about vectors using an smt theory of sequences

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett, and Ce- sare Tinelli. Reasoning about vectors using an smt theory of sequences. InInternational Joint Conference on Automated Reasoning, pages 125–143. Springer International Publishing Cham, 2022

work page 2022
[37]

Automated verification of consistency in zero-knowledge proof circuits

Jon Stephens, Shankara Pailoor, and Isil Dillig. Automated verification of consistency in zero-knowledge proof circuits. InInternational Conference on Computer Aided Verification, pages 315–338. Springer, 2025. 24 E. Pertseva et al

work page 2025
[38]

Formal verification of sp1 hypercube.https://blog

Succinct.xyz Blog. Formal verification of sp1 hypercube.https://blog. succinct.xyz/nethermind-lean/, 2025. Accessed: 2025-12-07

work page 2025
[39]

zkfuzz: Foundation and framework for effective fuzzing of zero-knowledge circuits

Hideaki Takahashi, Jihwan Kim, Suman Jana, and Junfeng Yang. zkfuzz: Foundation and framework for effective fuzzing of zero-knowledge circuits. arXiv preprint arXiv:2504.11961, 2025

work page arXiv 2025
[40]

Ligetron: Lightweight scalable end-to-end zero-knowledge proofs post-quantum zk-snarks on a browser

Ruihan Wang, Carmit Hazay, and Muthuramakrishnan Venkitasubrama- niam. Ligetron: Lightweight scalable end-to-end zero-knowledge proofs post-quantum zk-snarks on a browser. In2024 IEEE Symposium on Se- curity and Privacy (SP), pages 1760–1776. IEEE, 2024

work page 2024
[41]

Mtzk: Testing and exploring bugs in zero-knowledge (zk) compilers

Dongwei Xiao, Zhibo Liu, Yiteng Peng, and Shuai Wang. Mtzk: Testing and exploring bugs in zero-knowledge (zk) compilers. InNDSS, 2025

work page 2025
[42]

Bit- precise reasoning via int-blasting

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit- precise reasoning via int-blasting. InInternational Conference on Verifica- tion, Model Checking, and Abstract Interpretation, pages 496–518. Springer, 2022. A Proofs of Termination and Soundness of Translation Theore...

work page 2022
[43]

The next four rules decrease the second entry, without changing the first one

(Figure 4a lines 3-4: Consider the tuple ordering (number ofΣF-equalities inΓ, number of operators insidetoNat, number ofmodoperators, number of+ FP after− FP in all formulas, number of unbounded variables inΓ) sqrBdsandinjNatdecrease the first entry.mvZModSubdecreases the second to last entry without changing the first three. The next four rules decrease...

work page
[44]

Figure 4b lines 7-8:injBVLeqHypdecreases the number ofΣN hypotheses in Γwithout a correspondingΣ BV hypothesis

work page
[45]

Theorem 2.Soundness: For any contextΓ, the bitvector translationΓ ′ pro- duced byto_Nandto_BVfromΓis valid if and only ifΓ ′ is valid

(Figure 4b, lines 10-11) Consider the tuple ordering (number ofΣN-equalities inΓ, number of operators insidetoNat).injBVdecreases the first entry, and all subsequent rules decrease the second without addingΣN-terms. Theorem 2.Soundness: For any contextΓ, the bitvector translationΓ ′ pro- duced byto_Nandto_BVfromΓis valid if and only ifΓ ′ is valid. Proof....

work page