Reading through Bhatt-Morrow-Scholze’s “Topological Hochschild Homology and Integral p-adic Hodge Theory” I encountered the following statement.

We use only “formal” properties of THH throughout the paper, with the one exception of Bökstedt’s computation of $ THH(\mathbb{F}_p)$ …

As a reminder, Bökstedt (and Breen?) computed $ \pi_{*}THH(\mathbb{F}_p)$ as $ \mathbb{F_p}[\sigma]$ , where $ \sigma$ is a polynomial generator in degree 2. Whereas ordinary (derived) Hochschild homology of $ \mathbb{F_p}$ is easily seen to be a divided power algebra generated in the same degree, $ \mathbb{F}_p\langle x\rangle.$ Note that in the latter algebra, writing $ x^p = p! \frac{x^p}{p!}$ gives $ x^p = 0,$ quite a different flavor than the topological theory.

At some point I looked this up and the computation appeared to rest on some not particularly formal spectral sequence manipulations which I was unable to follow. Is this still the situation? Has anyone revisited these computations recently?