@DenisNardin I did mean the TAF book by Behrens-Lawson, although presumably there are applications to tmf as well.

@skd the TAF book is surprisingly user-friendly, and self-contained. The first 7 chapters (out of 15) tell you all the number theory you need to know, and after that it's pretty easy to construct. Saying something about TAF is, of course, much harder :)

@skd higher-dimensional formal groups are used to build $TAF$, by splitting off a 1-dimensional guy from its $p$-divisible part (if memory serves me). That's the only example I know.

@Ofra my group theory is a little rusty, so maybe I'm spouting nonsense. But my reasoning was as follows: if $N \rightarrowtail G \twoheadrightarrow G/N$ and $\psi$ is a generalized Euler characteristic, then $\psi(G) = \psi(N) + \psi(G/N)$, so by induction $\psi(G) = \sum_S \psi(S)$, where the sum is over the multiset of composition factors of $G$. Conversely, for a simple group $S$, we can let $\chi_S(G)$ be the number of times $S$ appears as a composition factor of $G$, and this is a well-defined Euler characteristic. I expect that $K_0(\mathbf{FinGrp})$ is generated by the $\chi_S$.