The Road to Divisors in #Monero What do you do when experts disagree? Three independent reviews, two years of work, and now a machine-checked proof. Learn more ⬇️ https://magicgrants.org/2026/09/29/Divisors-in-Monero

zkSecurity announced that they have formally verified the techniques of Liam Eagen's https://eprint.iacr.org/2022/596 in Lean 4, using only the standard axioms: https://magicgrants.org/2026/09/29/Divisors-in-Monero https://github.com/zksecurity/eagen-divisor-formalization X thread: https://x.com/zksecurityXYZ/status/2104953772669808866 "These techniques allows the construction of *extremely* cheap proofs of inner products relations on elliptic curves inside circuits; as long as linear combinations are free. However, it relies on some relatively involved/subtle algebraic geometry and both the analysis and the implementation are potentially easy to get wrong. We think that formal verification can solve this. Because we can verify both the protocol and then tie it back to verified Clean (https://clean.zksecurity.xyz) circuits implementing the technique. So since spring, we spent time, on our own initiative, to formalizing this. It was done by guiding AI through the techniques in https://blog.zksecurity.xyz/posts/divisor-notes/ , as well as carefully writing and reviewing the central theorem statements. The most interesting of which is soundness of the Merlin-Arthur protocol at the heart of the technique ("ma_soundness" in the formalization). For more details on the protocol itself, see our original report: https://blog.zksecurity.xyz/posts/divisor-notes/divisor-techniques.pdf"