Is formal verification specification writing similar to writing a more complicated property test? I’ve found writing property tests to be kinda difficult and time consuming for non-trivial programs.
Similar, not always the same. Property tests generally work at the interface of a system (either down to the function/procedure level or higher level) where you specify a description of the inputs and test the outputs satisfy some property or set of properties.
This will look a lot like what you do with formal verification at the same level. Formal verification tools can go deeper, though, like answering questions about the state of the system internal to a computation. Like "I have this loop invariant, can I prove (or have a system prove) that it actually holds across all iterations?" or "Can I prove that while doing this computation there is never underflow/overflow in any intermediate computation?" The former could be done with property testing if you pull the loop kernel out into its own procedure and then test the invariant property by executing the kernel with a large number of intermediate states. The latter is harder to do without really, really tearing your program apart down to the level of making each line separately executable.
I think my main point is that writing the specification is difficult enough with a non-trivial program with property tests, with many places tending to even avoid it if they can. If formal verification is even more difficult, it doesn't matter that it has more power and can make the code even more correct - the cost is a huge blocker.
It depends on how you do the formal verification. There are systems like SPARK/Ada which brings the specification into the language you're developing in (supports only a subset of Ada, but every year they're expanding what it covers), JML which does something similar for Java but the specification language is expressed in its own notation in Java comments, and others.
If you use these kinds of systems you can be more judicious in what you try to prove. Whole program proofs are infeasible (or at least impractical) generally, but you pick the subsets you care about most and you can add annotations and prove them (automatically ideally, but you can bring in an external proof assistant as well). You leave the rest of the system to testing which has proven remarkably effective over the decades (when taken seriously, at least).
This isn't an all-or-nothing proposition, you choose how to spend your time and effort with formal verification just like you do with testing or other work.
There are some specifications that are always there, like the absence of reachable panics or the backward compatibility between releases on stable entry points.
Otherwise you can outsource this work to specialized companies such as Formal Land or others!
