Say we design a simple Turing machine that adds two numbers together. Is there any way to formally prove that the machine actually computes the function we 'know' it does?
Is there a general method for all functions? Induction seems the most relevant, but will it work for any function? Any proof for this?
On
The only practical hope you have to be able to prove this is to develop your Turing machine (or program) carefully, making sure that you can prove that each step does its job correctly, and that the combination of steps is right. To convince a third party of its correctness, you'll have to provide the detailed reasoning behind each of the above steps.
On the other hand, Knuth famously said "Beware of bugs in the above code; I have only proved it correct, not tried it." There have been famous failures with formal verification done by hand.
This subject is known as formal verification in computer science, and people have done a lot of work in it.
For a sufficiently general version of the question, and with a reasonable notion of proof, the answer is no. Any notion of proof $T$ to which the incompleteness theorems apply suffers from the following limitation. Suppose we write down a Turing machine which searches for a proof of a contradiction in $T$, and returns $1$ if it finds such a proof (and doesn't return otherwise). If $T$ is consistent, then this Turing machine is supposed to compute the partial function which never returns. But if we could prove that in $T$, then $T$ could prove its own consistency, which contradicts the incompleteness theorems. (In fact it's possible to use this kind of reasoning to prove the incompleteness theorems from the undecidability of the halting problem.)