D.W.'s answer is great, but I'd like to expand on one point. A specification is not just a reference against which the code is verified. One of the reasons to have a formal specification is to validate it by proving some fundamental properties. Of course, the specification cannot be completely validated — the validation would be as complex as the specification itself, so it would be an endless process. But validation allows us to get a stronger guarantee on some critical properties.
For example, suppose you're designing a car autopilot. This is a pretty complex thing involving a lot of parameters. Correctness properties of the autopilot include things like “the car will not crash against a wall” and “the car will drive where it's told to go”. A property like “the car will not crash against a wall” is really really important, so we'd like to prove that. Since the system operates in the physical world, you'll need to add some physical constraints; the actual property of the computational system will be something like “under these assumptions regarding materials science, and these assumptions regarding the perception of obstacles by the car's sensors, the car will not crash against a wall”. But even so, the result is a relatively simple property that is clearly desirable.
Could you prove this property from the code? Ultimately, that's what's going on, if you're following a fully formal approach¹. But the code has a lot of different parts; the brakes, the cameras, the engine, etc. are all controlled autonomously. A correctness property of the brakes would be something like “if the ‘apply brakes’ signal is on then the brakes are applied”. A correctness property of the engine would be “if the clutch signal is off then the engine isn't driving the wheels”. It takes a very high-level view to put them all together. A specification creates an intermediate layers where the different components of the system can be articulated together.
In fact, such a complex system as a car autopilot would have several levels of specifications with varying amounts of refinements. A refinement approach is often used in the design: start with some high-level properties like “the car will not crash against a wall”, then figure out that this requires sensors and brakes and work out some basic requirements for the sensors, the brakes and the pilot software, then refine again those basic requirements into a design of the component (for the sensor, I'm going to need a radar, a DSP, an image processing library, …), etc. In a formal development process, each level of specification is proven to meet the requirements set by the level above it, all the way from the highest-level properties down to the code.
It's impossible to be sure that the specification is correct. For example, if you got the physics wrong, the brakes might not be effective even though the math relating the brake code to the formal requirements is correct. It's no good to prove that the breaks are effective with 500kg of load if you actually have 5000kg. But it's easier to see that 500kg is wrong than to see inside the brakes code that they won't be good enough for the physical parameters of the car.
¹ The opposite of a fully formal approach is “I guess this works, but I can't be sure”. When you're betting your life on it, that doesn't seem so great.