A model checker automatically verifies whether a formal model satisfies a given specification or produces a counterexample showing how it fails. We present a new way of using the counterexample to actively control a group of autonomous vehicles online in traffic. Each vehicle provides its own set of driving rules (requirements) about how it wants to traverse through traffic. The model checker is asked to prove the wrong specification that there are no trajectories such that the requirements of all vehicles are obeyed. Thus, we provoke a counterexample to the negated statement of what we are actually interested in, a solution to the driving task of the whole group. The resulting behavior is white-box, provably correct, and directly emerges from the requirements shared by the vehicles, without the need for an explicit implementation layer. Initial experiments with an open-source HighwayEnv implementation using the nuXmv model checker indicate that small fleets could be guided in real-time, and we see great potential for performance improvements by customizing the model checker for this task.