I like starting with defining outcomes, determining invariants, and then consider TLA+ or Lean models, or both. It's generally not good to ship stuff you don't understand, but if you work on big legacy code bases from 20-30 years ago, there's probably no one who understands all the code all the time.

It's at least nice to be able to prove something about the code, rather than blasting it with tests which only prove that the tests that are written do not fail (and perhaps get you some amount of code coverage — necessary but insufficient for anything like quality).

How to do all of that in your environment? That can vary greatly!