How do you encode the difference between a method that adds and a method that multiplies two numbers in the type signature?
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).
var x: int = y + 5
Here x is the variable being defined, it is declared to hold values of type int, and its initial value is given by the term y + 5.
In many mainstream languages, types and terms live in distinct universes. One starts by asking whether types and terms are all that different. The first step in this direction of inquiry is what are called refinement types. With our imaginary syntax, you can write something like:
val x: { int | _ >= 0 } = y + 5
Once again, x is the variable being defined, it is declared to always hold a value of type int at all relevant instants in all executions, and that its initial value is given by the term y + 5. But we additionally promise that x will always hold a non-negative value, _ >= 0. For this to typecheck, the typechecker must somehow also confirm that y + 5 >= 0.
But anyway, we have added terms to the previously boring world of types. This allows you to do many things, like so:
val x: int = ... val y: int = ... val z: { int | _ >= x && _ >= y } = if x >= y then x else y
We not only declare that z is an integer, but also that it always holds a value that exceeds both x and y.
You asked for the type of a function that multiplies two numbers. The type would look weird, so let me show you an imaginary example of the type of a function that computes the maximum:
val f : (x : int) -> (y : int) -> { int | _ >= x && _ >= y } = ...
This doesn't really get you to the maximum, because f might be computing max(x, y) + 5, but it does show the idea.
The final step in this direction is what are called full-blown dependent types, where the line between types and terms is completely erased.
Perhaps { int | _ >= x && _ >= y && (_ == x || _ == y) } ?
I just proved in Coq that if all of these always hold for a function, the function coincides exactly with the max function.
These ideas have not caught on for a reason. You end up writing the logic twice, and pretty high chances you mess up once.