It's not that TDD is incompatible with having formal requirements. It's that "Agile" Scum/XP etc. refuse to use the "R" word. The role of having requirements needs to be filled by some other means. For example, the Acceptance Criteria written on the back of the Story Card. TDD and Agile are often used together. Without formal requirements going into a large effort (not a single "story" but a full design that will comprise many stories) something has to take the place of the Requirements. That is often the TDD process.

So if you are using pre-written test cases instead of a document of formal requirements, then it's important to do a good job of it and indeed to write them first.