Of course if one wants to avoid coordinates then one should replace formal group laws by the coordinate-invariant things that they are the coordinate-dependent versions of!

There are two dual ways to do this that I know of.

**Commutative:** First, observe that an $n$-dimensional formal group law over $k$ is precisely a comultiplication on $k[[x_1, ..., x_n]]$ (with respect to a suitably completed tensor product) with counit the map that kills all terms of positive degree and antipode the map that multiplies each monomial by $(-1)^{\text{deg}}$. This gives $k[[x_1, ..., x_n]]$ the structure of a commutative Hopf algebra (in a suitable category of power series algebras equipped with a suitably completed tensor product) and now we can ask how to construct this Hopf algebra from $G$. This can be done by considering the completion of the algebra of germs of smooth functions at the identity of $G$ with respect to the ideal generated by the germs vanishing at the identity. The comultiplication is induced from the multiplication $G \times G \to G$ via pullback of germs.

**Cocommutative:** First, recall that if $\mathfrak{g}$ is a Lie algebra then the universal enveloping algebra $U(\mathfrak{g})$ is naturally a cocommutative Hopf algebra. In fact over a field of characteristic zero the functor $\mathfrak{g} \mapsto U(\mathfrak{g})$, when regarded as taking values in Hopf algebras, is full; by PBW $\mathfrak{g}$ is precisely the Lie algebra of primitive elements of $U(\mathfrak{g})$. Hence we should be able to identify Lie algebras with a certain full subcategory of Hopf algebras.

**Theorem (Cartier):** Let $k$ be a field of characteristic zero. A Hopf algebra over $k$ is isomorphic to the universal enveloping algebra $U(\mathfrak{g})$ of a Lie algebra over $k$, namely its Lie algebra of primitive elements, if and only if it is cocommutative and conilpotent.

The definition of conilpotence is mildly involved but see, for example, Cartier's A primer of Hopf algebras.

Now I claim that $U(\mathfrak{g})$ should be seen as a version of the formal group law associated to $\mathfrak{g}$. The reason is that as a Hopf algebra it is dual in a suitable sense to the Hopf algebra above. So Cartier's theorem should be seen as a coordinate-independent version of the correspondence between Lie algebras and formal group laws which in particular does not require Baker-Campbell-Hausdorff.

It remains to figure out how to get $U(\mathfrak{g})$ directly from $G$, and the answer is the following:

**Theorem (Schwartz):** $U(\mathfrak{g})$ can naturally be identified with distributions on $G$ supported at the identity.

(The dual pairing between the two Hopf algebras above is then the natural pairing between distributions supported at the identity and germs at the identity.)