Given a system, and its complete state space, can I say that that state space is a formal specification of that system's behaviour?
Not unless you have formally defined all possible transitions to and from each state and your state space is inclusive of all possible states the system can be in.
In a formal definition for a computer system, it should also include unexpected transitions such as computer crashes. A fault tree analysis may help with ensuring that all possible states are defined.
See wikipedia