Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state?
No.
Take a simple function that has two 64-bit numbers as input and one output; your sixteen 4Ghz cores would take over 11 billion times the current age of the universe to verify it.
You can, instead, do things like symbolic execution... and it turns out, that kind of thing is often a big part of "formally proven correct".