For the reasons given by Gilles, there can't be a formal system that represents all total computations. If you had such a system, you'd have a system equivalent to all halting Turing machines. But the halting problem tells us that you can't decide if a machine halts or not, so you wouldn't be able to decide if an element (a Turing machine) belongs to the system or not.
However, you can get very close. Good formal models for this problem are (strongly) normalizing typed lambda calculi. This means that every term has a normal form - a definite result that you can obtain by a finite number of application of reduction rules. In other words, every computation has a result, every computation is total. The stronger system you have, the more total functions you can express in it (although you can never express all).
A nice example is System F, also known as the polymorphic lambda calculus. There is a theorem that says that
A function (on natural numbers) is expressible in System F if and only if it can be proved in the second order Peano arithmetic that the function is total.
This means that in System F you can express basically all imaginable total functions. So although you can't express all total function, you can express all total functions for which you can prove they're total, which is basically the best thing you can do.
There is a bit weaker system, Gödel's System T, for which there is a very similar theorem for first order Peano arithmetic. However this system is not as nice as System F. (In System F you can represent natural numbers, booleans etc. natively, while System T is constructed as the simply typed lambda calculus with externally added naturals and booleans. Also System F has type polymorphism, which makes it much more elegant in many cases.)
You can find all the details about these systems in Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0-521-37181-3.
Coq is based on a even stronger calculus of constructions, which is also strongly normalizing, so in Coq you can describe even more total functions.