The truly paranoid would never believe any algorithm is immune to faults.
Even if full mathematical code analysis shows it to be so, can you prove that the proving analysis algorithm itself is immune to faults? It is potentially faulty turtles all the way down!
The proof checker can be ran several times to account for faults. Then you don't need to run it at all (it's proven). And you can use another proof checker (or that proof checker itself) to prove that the proof checker works. Etc.
Now there's the problem of the compiler, which gives a upper bound on the confidence you can have: if there's a bug in it, you're screwed even with a correct algorithm.
> Even if full mathematical code analysis shows it to be so
Come to think of it, that may not be possible for lots and lots of algorithms —whose mathematical security is only conjectured to begin with. Thanks for pointing that out.
But you can prove many things. Many programs we care about can be proven correct (for whatever definition of "correct" we manage to formally specify), and those we can't prove correct can probably be transformed into provable versions —assuming they're short enough.
A better question would be whether, in a theoretical sense, fault-free algorithms even exist. There are similar questions, like whether one-way functions exist, where we have lots of evidence to suggest that the answer is "yes" but we have yet to prove it.
This is what SEL4 people are doing.
The remaining part is verifying if your machine model is correct. Not trivial for some CPU and memory controller as complex as x86. (Even though just a subset of operations are used.)
Doing this also allows you a proof against fault attacks and timing attacks.