The issue is I’ll have to vibecode all the laws and the laws could be wrong.

writing specs is hard. For instance the easiest way to comply with "player should never reach the flag" is to disable movement completely, so then you have to specify "player should never reach the flag while still being allowed to move" and so on (liveness). It's not practical for most programs

Jokes aside, I think the idea is that the law is simple to code, the proof that it holds is where the agent is responsible. This probably becomes less true though as you try to express more complicated laws.

Words of wisdom.

true