Every book of mathematical logic should be a good reference where to find the notion of formula.
Usually when one refers to formulas it means formulas of a first order language.
A first order language is specified by a family of symbols of three types: constants symbols, function symbols and predicate or relation symbols.
From this symbols and the variables you can build all the terms and formulas.
Basically terms are either variables, constant or sequence of the form $f(t_1,\dots,t_n)$ where $f$ is a function symbol and $t_1,\dots,t_n$ are terms (this is a sort of recursive definition, one that can be codified in a formal grammar indeed).
Formulas are defined in a similar (recursive) fashion: a formula is either an equation of the form $t_1=t_2$ where $t_1$ and $t_2$ are terms, a predicate of the form $P(t_1,\dots,t_n)$ where $P$ is a predicate symbol and $t_1,\dots,t_n$ are terms, or a combination obtained from this basic (atomic) formulas via connectives and quantifier application.
My apologize for the absence of details but you can really find all this stuff in every basic book on the subject.
For your question about the regularity of the grammar, at the moment I don't have any proof but my guess is that a first order language isn't a regular one. I suppose that using pumping lemma could be constructed strings that aren't first order formulas. If that would be the case then I such kind of language, the set of first order formulas of a first order language can't be regular.
Hope this helps.