Modern formal methods like TLA+ and Alloy are as easy to pick up as Python, and other than having to write a spec (an ultra-simplified model of part of a system) they are completely automatic (based on model checkers). There is no reason for a modern software engineer not to have them on her radar. As a matter of fact most of the cloud systems you are using everyday have been verified with modern formal tools: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB, ... and many others.
You are going to have requirements whether you like it or not. It doesn't matter if you discover them during requirements engineering and validate and deconflict them on a simple text document, or if you discover them as you go during coding (possibly after having coded the wrong thing), or if the client discovers them during the "sprint review" of some allegedly agile cult. The only difference is how much money and time are you willing to trade for being called "agile". Ironically the traditional way of doing a requirements stage is the less expensive of all three options. It is also the most aligned with the original agile spirit, since it converges with the client as soon as posible, at the point where changes are the most cheap (changing a line on a text document).