Formal systems (like formal axiomatic set theory) are more in the domain of logic than mathematics (although there are things like model theory that lie at the intersection of the two). From their very early conception, they were designed to serve two roles: 1. Serve as completely precise languages, where no ambiguity is possible, and 2. allow for mechanical reasoning. As role 1 is often in service of role 2, I think it's fair to generalize and say that the role of formal systems is mechanical reasoning.

If mechanical reasoning is not something that interests you, you have little use for these pedantic systems. Mechanical reasoning has two current uses: 1. mechanical verification of mathematical proofs and assistance in such proofs -- this application is very rarely used in practice, and is commonly the domain of a few enthusiasts who hold high hopes for improvements that would make it more mainstream. 2. Mechanical verification of software, including static analysis, model checkers, type systems and other software-relevant proof systems.