Binius64 Roadmap

Features

We are planning to add several important features:

• Recursion. Proof composition and recursion are important techniques for proving large statements, while bounding memory usage.
• Succinctness. While Binius64's proof sizes are succinct, its verification complexity is not yet. We are working on achieving succinct verifier complexity and reducing verification times.
• Formal verification of circuits. We would like to develop a framework for writing circuits in Lean4 and formally proving their security properties.