Where in the toolchain does formal specification come in?
Tests can be written based on either a formal spec or an informal spec.

Verification always requires a formal specification.  Formal verification might be manual or automated, or some combination of the two; it depends what techniques you use.  Typically, it's hard to do completely automatic verification -- it's more usual that verification systems automate part of the verification task, but require some assistance from the programmer (e.g., to specify invariants or prove lemmas that are hard for the automated system to prove).  See https://en.wikipedia.org/wiki/Formal_verification for an overview; there are also textbooks that give an overview of formal verification.  I suggest reading some standard references on formal verification: they will probably answer a lot of questions you might have.

There's nothing that says you have to have an informal spec, a formal spec, and a program.  You could have just a formal spec and a program.

It is often helpful to have specifications at multiple levels of abstraction/granularity, with theorems relating them.  Higher-level specs may be easier to understand and specify properties about the whole system or properties we ultimately care about, but may be difficult to prove directly; lower-level specs may be more detailed and harder to work with or understand, but may have a more direct mapping to the program and might facilitate proof/verification.

Higher-level specs might be formal, or in some cases they might be less formal.