Abstract interpretation (esp Astree Analyzer) at top for ease of use in static analysis. Fire and forget mostly. Model checking next because you just learn specifications and certain ways of structuring code for easy analysis. Theorem proving last for where it's worth the specialist labor and long turnaround (eg kernels, compilers, SSL).
That's been my order for years. Empirical evidence supports it so far.
