That depends on what you want to use formal methods for. For full functional correctness, yes, you need a spec. But much can be gained by just proving the absen

That depends on what you want to use formal methods for. For full functional correctness, yes, you need a spec. But much can be gained by just proving the absence of runtime errors, i.e., for C, things like "all array accesses are in bounds", "every dereferenced pointer is valid", or "integer arithmetic never overflows". Formal methods tools for C have those baked in, so you can get going quickly without specifying these things yourself. It's still hard, though.