AI can generate a plausible implementation of anything, which moves the bottleneck from writing code to knowing it's correct. A working pipeline — behavioural specs, synthesised Yul, machine-checked refinement — and why the only component you have to trust is the checker.