That's up to the harness. Right now, my harness doesn't have any tools that would allow the agent to change contracts. Also, agents working on a Rocq proof don't have write access to the C+ACSL code; they can review it, and propose structural changes to the coordinator, but all they can do is iterate on the Roqc proof or give up. The weakest part of the harness today is that the agents that do C+ACSL work can modify both C and ACSL, even though they're usually run with the explicit intent to not change the semantics of the C code (although it's totally within bounds, and often required, for them to change e.g. `foo & 3` to `foo % 4`) -- so there's weakness here, but it's bounded, and since the contracts live in header files that they can never write, it's worked so far. It's a starting point, at least; I certainly wouldn't say this is a mature, or even good, tool chain, but still learning.