That being said, FM is an enormous spectrum; if you squint a little, writing really good user stories could be considered a 'formal specification'. There's a really good paper from Amazon about model checking (Newcombe 2014 IIRC) where they make the bold statement that "Doing the math didn't help us find that many mistakes, nor did using the model checker; the thing that was most helpful was sitting down and forcing ourselves to come up with really good definitions. Like what does X really mean?" So it doesn't have to be as complicated as you think.
So if you want to start as simple as possible, I would recommend something like this: https://www.hillelwayne.com/post/decision-table-patterns/