2026-11-06 –, Lotus Stage 3
I’ll evaluate autoresearch approaches from AlphaEvolve and AI theorem provers to zk.golf and SNARK.fast through a common ZK optimization harness, grounded in Atheon’s ProveKit and WHIR work. I’ll run experiments on SHA-256/R1CS and polynomial commitments, ACIR to R1CS lowering and WHIR folding parameters measuring constraints, witnesses, proving time, memory and proof size to see which agent, verifier and reward setups actually find correct, useful optimizations, security findings.
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.
Rose is a ZK and protocol engineer at Atheon, working on ProveKit, cryptographic optimization, and Trinity. Previously, she worked on MEV infrastructure at Primev, applied cryptography at ZK Email, and Ethereum protocol research through Nethermind and the Ethereum Protocol Fellowship. She also contributes to Prysm, Reth, and rust-libp2p.