Program Synthesis & Verification: Counterexample-Guided Search (2D)

This 2D companion strips the CEGIS search visualiser down to a flat radial plot: the specification becomes a jagged closed curve around a center point, and each candidate program is a dot at some angle and radius. Guided refinement pulls a dot's radius toward the boundary using the signed distance as its counterexample signal, while random search jitters blindly — the same loop as the 3D version, easier to read because everything sits on one plane instead of orbiting in space. Watch the color shift from red (far from verified) through amber (close) to green (verified) as the population converges, and compare how much faster CEGIS closes the gap than blind search on the same specification.