-- Modeling: You start with basics like using the small universe assumption to bound checking to X transactions. I'd expect most front running to show up as small cycles here, so the typical case is a super small X. Later, you might get into a time cost semantics to better tune what you consider interesting, but almost no one in the crypto space is at the level of modeling maturity. I'd predict a team's time is way better spent building up a stdlib of contract checks, verified contract helpers, & whitebox attack heuristics/guides.

-- Modeling II: Also, in verification, it's way better (ex: realizes more of the ROI) to verify the program has the properties you want ("money goes from a->b without getting stuck"). You can dream up individual attacks and model those one by one ("front-running where ..."), but then you potentially miss some, or some aspect of one. That's basically the difference between verification and testing. You still do stuff like check sample scenarios & individual attacks, but that's more about testing the verification conditions & model fidelity.

-- Fixes: A good (while still cheap & easy) checker gives you summarized examples of attacks. Likewise, it makes it interactive, so you can tune what you consider in/out of scope. More R&D-level verifiers suggest patches (verification and synthesis are two sides of the same coin), but that's not necessary. If your idea sucks or the attack is unavoidable, the verifier isn't the problem, and if you decide to still proceed with the now proven-bad idea, you can at least now price the risk in.