[ted_dunning]

It is hard to understand what you mean by type signature, but I think what you mean is something like the type signature in Java, Go or C.

That isn't what people are talking about when they talk about formal verification with a type system. They are talking about much more complex type systems that have equivalent power and expressivity to formal logic.

This intro is good at introducing the topic. Unfortunately, the correspondence between advanced type systems and logic is itself fairly abstract and uses lots of concepts in non-intuitive ways. This means that you can easily wind up in a situation where you can do lots of proofs about number theory using a tool like Lean4, but you don't really see the corresponding types (this is what happened to me).

https://leanprover-community.github.io/learn.html