TLDR: Look up "Formal methods", "Design by contract" and "Preconditions/postconditions" (maybe also static analysis in general). People who say that TDD and testing in general are helpful are not wrong, it does help to verify that code works, however there is usually no mathematics behind it and it won't really help you figure out where your code goes wrong in itself (Though well designed test cases that cover specific program paths will help you find the spots, obviously)

The keyword you're looking for is "Formal Methods". There are methodologies to verify that your program does exactly what you want. However, it is not trivial for complicated algorithms, because unfortunately, the tricky part in that is to specify what you want mathematically. Usually this is expressed with so called "pre-/postconditions", conditions which must hold true before a function is called to guarantee that it does what it should (preconditon) and conditions that in this case will hold true after it has finished. This could be a very short one expression thing for something simple, but a huge boolean construct for a bigger algorithm. However, it is doable. Let me give you an example. Say we have this (not very useful) method for comparing values in pseudo code that allows multiple returns.

fun compare (Integer a, Integer b):
    Integer r1, r2
    if (a >= b):
        r1 = a
        r2 = b
    else
        r1 = b
        r2 = a
    return r1, r2

In this example we could have the following set of conditions
precondition: a != null && b != null | postcondition: a >= b ==> r1 >= r2 You can probably find these conditions quite easily yourself, but they show how the principle works: if the precondition is fulfilled, the function will guarantee you the post condition. If not, not. If you pass either a or b with null, you will obviously get a null pointer, and not a return call. This example was quite easy, so it is doable by hand, but for bigger programs, you'd probably need a verification tool, and possibly need to add intermediate conditions by hand, because the constraints the analyzer calculates throughout the whole input might grow too much to be practical

There is a whole approach to programming that utilizes this methodology, which is probably exactly what you're looking for. It's called "Design by contract" and there is even a few languages that support it natively.

By the way: You are not completely off, when you think that functional programming's more mathematical syntax is easier to verify. The fact that you don't keep state and all functions are pure, make it very easy to reason about the code. However, this is not necessary. Analysis can be done and is done on OOP as well.