Unit tests do not verify behavior, except for a few cases (out of a virtually infinite set of cases) that the programmer happened to think about.

Types do verify behavior - e.g. this function always returns an Int, that function only returns a UserId, this other function doesn't do any I/O.

That is a very different behavior though. If my multiply function returns ADDs the input and returns an int it passes the type checker but is still wrong.

But if your multiply function fails to handle some special case that the tests don't catch (negatives, overflow/saturation, denorms, ...) then the tests are also wrong.

What you really want is to be able to state properties, e.g. "for all x/y, mul(x, 0) = 0, mul(x, 1) = x, mul(x, 2) = x + x, mul(x, y) = mul(y, x)", and so on. And working with these kinds of statements (via e.g. quickcheck or whatever) might generate tests, but feels a lot more like working with types. You're making proofs, not examples.

Which is why I have always (well for the last 5 years or so anyway) said that you want both because they catch different issues.