Use tla+ and have it go back and forth with you to spec out your system behavior then iterate on it trying to link the tla+ spec with the actual code implementing it
Pull out as many pure functions as possible and exhaustively test the input and output mappings.
The problem with specs for me is always with boundaries. How many specs do you have for a complex project? How do they reference each other? What happens when requirements cross boundaries?
And finally, how do you address spec drift?