Recent work on Veridium has not changed character. It continues to be brutally difficult, with problems having subtle causes that are hard to diagnose. Here is the short version of the recent progress:
- Switching from Binius v0 (stale fork) to Binius v0 (HEAD), and currently at 53 tests, all passing
- Adopting some Binius M3 primitives this time
- Embracing formal verification
- Growing coverage of the circuits using Kani
- Plans for implementing Z3 and a hash-adapted fork of Decree
- Many new probes, audits, and diagnostics
Current status: Ready to start on the recursion assembly now. This will compose all of the working recursion segments into a single multi-segment block with fully wired data-level integration residuals and assembly-dependent gates.
Disclaimer: Deep Veridium Lore AheadThis rest of this post has three goals:
1. Provide a clear picture of the recent difficulties that Veridium has encountered and the solutions that were found.
2. Explain how Veridium rests upon Binius as a substrate, without which it could never have been built.
3. Justify the particular version of Binius in use (v0) versus alternatives like the newer and actively maintained Binius64.
Troubles with Multipoint-Opening Veridium recently reached a point where proving the Merkle membership in-circuit FRI verifier was among the final remaining tasks. The system must prove that the coset symbols the circuit folded are the same ones that were actually committed. Without it, a malicious prover could fold any internally-consistent fake coset and the circuit would accept it. For soundness, this is effectively the core of Veridium's proof system.
The linkage mechanism required a multiset equality argument to prove that the set
{(query, round, M-coset)} from the fold side equals
{(query, round, bind)} from the Merkle/Grøstl side. However, because these lived on different rows with no copy/permutation primitive available, this required some form of grand-product or running-product check.
Why BiniusBefore I explain the various failed approaches, it's important to consider what the Binius library is and why it is the foundation of Veridium's design.
Binius is the arithmetization substrate that everything else in Veridium sits on top of: the constraint system, the polynomial commitment scheme, the FRI protocol, the field tower. Choosing it was a foundational decision.
The people who built Binius were well-credentialed professionals. Irreducible assembled a serious team of cryptographers and systems engineers, funded at a level that reflected the significance of their research agenda. The math that they produced, particularly the binary tower field construction and the packed multilinear approach, is genuinely novel work. There are other libraries for ZK and STARKs, but Binius is still years ahead of them.
While I am devoted to understanding zero-knowledge proofs, much of the math and cryptography are still beyond me. As a proof system built by a world-class group of researchers, Binius is a strong foundation to build upon.
Three Failed ApproachesI tried three different approaches in my efforts to bring multipoint-opening to Veridium. I failed each time, but the pattern told me everything that the circuits couldn't.
Approach #1: The Helper PolynomialThe idea was to use Binius' included
msetcheck and
prodcheck features to commit a helper polynomial
f' and open it. The product-tree structure forced
f' to accumulate five distinct evaluation points, and
greedy_evalcheck simply cannot collapse a committed polynomial opened at multiple points into a single same-query PCS claim. That was the wall I was up against; though I still hadn't realized it.
Beyond the evaluation problem, the payload cost alone was fatal: supplying the roughly 2,200 trace evaluations needed to cover the batched commitment produced a proof in the 500-600 KB range, way beyond the current blockchain payload budget. Even if the evaluation collapse had worked, the approach just wasn't viable.
Approach #2: Isolating the TuplesThen, I thought that perhaps the problem was that the linkage tuples were entangled with the rest of the trace. The second approach moved them into their own dedicated committed batch, on the theory that a narrower, isolated batch would be easier for
greedy_evalcheck to handle. It was not. A dedicated batch still commits and opens
f', and
f' still accumulates the same five evaluation points from the product-tree structure. The same wall was there waiting for me, and so was the payload explosion. Isolating the tuples changed nothing about the underlying mechanics.
Approach #3: The Running-Product ColumnThis was the most promising of the three and, for a little while, it looked like it might actually work. This Plonk-style approach meant replacing the separate
f' commitment entirely with a single running-product column
z living directly in the trace. Because
z was riding the main trace commitment, it opened at the main point rather than accruing its own separate openings. The cost dropped to something manageable, and the Fiat-Shamir malleability analysis confirmed the approach was sound as long as the challenges were sampled after the trace was committed.
The prove-side wiring went in with
RunningProductComposition, the two-round commit structure, a
z_next shift, the composite batched into the main zerocheck, and the post-greedy split to open
z into the new proof fields. Then, I hit the wall again.
The
z column was referenced in two ways: directly, and through the
z_next logical-right-by-one shift. Each reference landed at a different evaluation point, giving
greedy_evalcheck two distinct points to reduce for the round-2
z batch. The main trace batch had an identical direct-plus-shift structure and collapsed successfully, but the fresh round-2
z batch did not.
Analysis: Hitting the Multi-Point Committed Polynomial Evaluation WallThree constructions, three different shapes, and each one ran into the same error. The prodcheck's
f' hit it at five points. The isolated tuple batch hit it at five points. The running-product column hit it at two points. The number of points changed but the failure mode didn't. I was now left with only one possible conclusion: the root cause was structural.
So, I went looking for answers and it didn't take too long to find out that I had made a major mistake in the early days of Veridium. Tempted by a feature I wanted, I built upon an older fork of Binius without checking how old it was. I now realize it lacked many of the features and decouplings of the latest version. A simple error in judgement had baked insurmountable flaws into the project from the start.
The stale fork featured a
greedy_evalcheck that was built around the assumption that every committed polynomial could always be reduced to a single same-query PCS claim. The reduction path to handle multiple evaluation points per committed polynomial was simply never finished or exercised. The
prodcheck and
msetcheck code existed, but the greedy opening path was never hardened for it in practice.
Every construction I attempted that needed to open a committed polynomial at multiple points would eventually reach the same incompatible assertion and fail.
Solution: Replace the SubstrateThe wall I kept hitting wasn't just another hard problem waiting to be solved. It was a fundamental property of the substrate I was building on, and the substrate needed to change.
By pivoting to an official copy of the latest Binius v0, I was able to resolve both the evaluation problem and the linkage architecture at the same time, and not through patches but through a fundamentally different design.
The first major structural difference is the separation of zerocheck and sumcheck into independent protocols. In the old fork, these were coupled, and the evalcheck machinery had to collapse each committed batch down to a single same-query point before it could proceed. Now,
greedy_evalcheck returns a flat list of
EvalcheckMultilinearClaim values with no per-batch collapse step, no
MissingEvals error, and no same-query assertion. The reworked FRI protocol opens multiple evaluation points per committed polynomial natively.
Another major improvement is the channels system, which is what makes Veridium's linkage genuinely clean now. The new
gkr_gpa (GKR grand-product argument) reduces a grand-product claim to an evalcheck claim on the existing committed inputs. No
f' to commit. No running-product
z column. No second commitment round and no extra opening of any kind. The linkage instead becomes a channel: the fold side pushes its
query, round, M-coset) tuples in, the Merkle side pulls them out, and the channel's multiset balance is enforced natively by the GKR argument over inputs that are already committed. The balance being correct is the binding.
What took three failed attempts and ton of work to approach on the old substrate took a single isolated test to validate on the new one. Channel-based linkage proved and verified on synthetic data, then balanced correctly on real genesis data, with tamper-rejection working in both cases.
Addendum: Binius v0 vs. Binius64It is true that Binius v0, the current substrate, is not being maintained and that Binius64 has superseded it. I had studied Binius64 for awhile, long before the multipoint-opening effort began, and my reasons for not adopting it still stand; for now.
Veridium's security model includes a predicted roughly five percent performance advantage for purpose-built hardware running the Rule 30 VDF. That gap is small enough to be meaningful as a mining incentive without being large enough to centralize the network, which is by design.
Binius v0's table-based arithmetization, with its binary tower fields operating at the bit level, is structurally more compatible with the kind of hardware arithmetization that could realize this advantage: FPGAs and custom ASICs that treat bitwise operations as native rather than mapping them down from 64-bit words.
By remaining on v0, Veridium maintains a hardware-compatible arithmetization that plausibly enables an easier path to validating that the predicted five percent mining advantage is preserved under custom hardware acceleration.
So this is not a permanent rejection of Binius64. The analysis done during the early research phases was based on the state of both systems at the time, and Binius64 continues to be actively developed. The tradeoff will look different once Veridium's untold hardware story is further along. For now, the v0 foundation is what makes the low-cost hardware mining thesis coherent, and that's reason enough to stay the course.
