Start with the money: which functions move value, and who can call them? Then map trust boundaries, external calls and assumptions. Ask what happens with zero amounts, the same address twice, a reentering token, or a paused oracle.
// checklist: access control, CEI, arithmetic, external calls, // initialisation, upgrade safety, oracle freshness, event coverage
Write the invariant in a sentence — "the contract always holds at least the sum of stakes" — then try to break it.