Tabby - A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits

Explore a 15-minute conference presentation introducing a synthesis-aided compiler that automates the generation of high-performance zero-knowledge proof circuits from high-level code. Learn how this innovative compiler addresses the challenge of translating high-level programs into arithmetic circuits while maintaining both correctness and efficiency. Discover the domain-specific intermediate representation designed for symbolic reasoning and understand how sketch-based program synthesis derives optimized low-level implementations. Examine the approach of decomposing programs into reusable components and verifying semantic equivalence through SMT-based reasoning to ensure correctness while achieving substantial performance improvements. Review evaluation results on real-world ZKP applications demonstrating significant reductions in proof generation time and circuit size compared to mainstream ZK compilers. Gain insights into advanced compiler techniques, program synthesis methodologies, and zero-knowledge proof optimization strategies presented by researchers from UC Santa Barbara, University of Illinois at Urbana-Champaign, University of Toronto, and Polychain Capital at the OOPSLA 2025 conference.