[ArkyBeagle]

"Proving correctness" is sort of windmill-tilting for today. Just don't despair of this :)

Good test vectors are a great investment, as are constraint checks and supporting instrumentation of said constraint checks.

[StrykerKKD]

I don't despair, because I know that to prove correctness of a program you need to use math.

For example proof assistants(like Coq, Agda, Idris, hol) are capable of proving correctness of a program.