Autoresearch for ZK Optimization

Duration: NaN:NaN:NaN

Speaker: Rose Jethani

Type: Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

Autoresearch systems use very different feedback loops: AlphaEvolve searches against executable evaluators, AI theorem provers use formal verification, and zk.golf combines Lean-checked circuit semantics with circuit cost. I’ll use these approaches as reference points for an internal autoresearch harness we built at Atheon to experiment with ZK optimization and evaluate how different verification and security tools perform within the loop. The harness lets agents propose and implement optimizations, checks them using formal verification, equivalence testing and circuit-security tooling, benchmarks valid candidates, and feeds the results into the next iteration. I’ll test this on ProveKit and WHIR workloads, including SHA-256 arithmetization, ACIR to R1CS lowering and WHIR folding parameters. I’ll compare constraint and witness reduction, proving time, peak memory and proof size across approaches, alongside verified-candidate rate, optimization success rate, security findings.