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.