The answer is affirmative, if one is careful about making the appropriate definitions (e.g., the test objects in the definition of formal smoothness, and the correct topology on the algebra of "formal power series" in an arbitrary set of variables). But I am not aware of any literature reference. This should have been included in SGA3, but appears to have not been addressed there.
The category you call $\mathcal{D}$ consists of exactly what are called "pseudo-compact" local $\mathcal{O}$-algebras with residue field $k$. The basic theory of such rings (without the locality or residue field conditions) is developed in sections 0 and 1 of Gabriel's Exp. VII$_{\rm{B}}$ of SGA3 building on earlier work of Gabriel, including the crucial notion of pseudo-compact module (and topological properties thereof, especially in relation to closedness of images of linear maps in the "pro-finite" case) and some parts are discussed (more like a survey than with full proofs) in sections 3 and 4 of Chapter 1 of Fontaine's Asterisque volume 47 on p-divisible groups.
This category admits arbitrary inverse limits (given in the expected manner topologically). Two key notions in the development are topological flatness and the appropriate versions of Nakayama's Lemma, and every pseudo-compact ring is topologically a direct product of local ones (and is noetherian if and only if it is a product of finitely many complete local noetherian rings).
The basic features of formally etale algebras are discussed in 1.6 of Exp. VII$_{\rm{B}}$, avoiding the locality and residue field conditions (except to show that in such cases it is a vacuous notion); the functorial condition uses artinian rings of finite length over the base as test objects. There is an equivalence in the local case with formally etale algebras over the residue field (which in turn are precisely topological products of finite separable extensions), but oddly enough the development of formal smoothness (again using artinian rings of finite length over the base as test objects) doesn't seem to be given there. The proof of an affirmative answer to the question posed is inspired by the more familiar noetherian setting but requires the versions of Nakayama's Lemma (see 0.3.3 of VII$_{\rm{B}}$) and (topological) flatness that are appropriate to the pseudo-compact setting.
Having said all of that, let's now give the proof which is requested. More generally, let $R$ be any local pseudo-compact ring (such as $\mathcal{O}$) and $A$ a formally smooth local pseudo-compact $R$-algebra with the same residue field $\kappa$ as for $R$. We claim that $A$ is a formal power series ring over $R$, and the proof will only require using artinian rings with that same residue field as test objects for the formal smoothness (as in the traditional setting). Note that $A$ is a "pro-finite" pseudo-compact $R$-module (i.e., inverse limit of finite-length discrete $R$-modules) due to the residue field and locality hypotheses.
Suppose the case of artinian $R$ were settled. Hence, for every open ideal $\mathfrak{a}$ of $R$, the pseudo-compact $R/\mathfrak{a}$-algebra $A \widehat{\otimes}R (R/\mathfrak{a})$ is formally smooth, thus topologically a formal power series ring over $R/\mathfrak{a}$ and so topologically flat over $R/\mathfrak{a}$. Rather generally, if $M$ is a pseudo-compact $R$-module and $M \widehat{\otimes}_R (R/\mathfrak{a})$ is topologically $R/\mathfrak{a}$-flat for all open ideals $\mathfrak{a}$ of $R$ then $M$ is topologically $R$-flat. Indeed, if $j:N' \rightarrow N$ is a closed submodule of a pseudo-compact $R$-module and $\{N_i\}$ is a cofinal system of open submodules of $N$ then $N'_i = N' \cap N_i$ is one for $N'$, and the inclusions $j_i:N'/N'_i \rightarrow N/N_i$ recover $j$ upon passage to the inverse limit. But $N/N_i$ is killed by some $\mathfrak{a}$, so the $R/\mathfrak{a}$-flatness shows that $j_i$ remains injective after completed tensor product against $M$ over $R$ (since same as for $M \widehat{\otimes}_R (R/\mathfrak{a})$ over $R/\mathfrak{a}$). The formation of completed tensor product commutes with inverse limits against finite-length objects, so the injectivity of $j \widehat{\otimes}_R M$ is established.
The upshot is that if the case of artinian $R$ is settled then $A$ is at least topologically flat over $R$. Let's see how to conclude from this. By the assumed settled case over the residue field $\kappa$, there is an isomorphism of pseudo-compact $\kappa$-algebras
$$f_0:\kappa[\![X_i]\!] \simeq A \widehat{\otimes}_R \kappa = A/\overline{\mathfrak{m}_R A}.$$
(Here and below, the overline denotes topological closure.) Since the target has the quotient topology, we
can lift the images of the $X_i$'s to elements $a_i \in \mathfrak{m}_A$ such that $a_i \rightarrow 0$, so we can lift $f_0$ to a continuous $R$-algebra map
$$f:R[\![X_i]\!] \rightarrow A$$
sending $X_i$ to $a_i$. This lift $f$ is surjective due to the formal Nakayama Lemma over $R$. Letting $I = \ker f$, the topological flatness (!) of $A$ implies that $I \widehat{\otimes}_R (R/\mathfrak{m}_R) = \ker f_0 = 0$, but this completed tensor product is $I/\overline{\mathfrak{m}_R I}$, so the formal Nakayama Lemma over $R$ implies $I=0$ and hence we are done.
In this way we reduce to the case when $R$ is artinian. Hence, by the formal smoothness hypothesis, the quotient map $A \rightarrow \kappa$ lifts to an $R$-algebra section $s:A \rightarrow R$. Let $J = \ker(s)$, and consider the pseudo-compact $\kappa$-module $V = (J/\overline{J^2}) \widehat{\otimes}_R \kappa = J \widehat{\otimes}_A \kappa$. This is topologically free, as is every pseudo-compact vector space over a (discrete) field, so we may choose a topological basis $\{\overline{e}_i\}$ (in particular, $\overline{e}_i \rightarrow 0$ in the topology of $V$). But $V = J/\overline{\mathfrak{m}_A J}$ with the quotient topology, so we can lift this to some $\{e_i\}$ in $J \subset \mathfrak{m}_A$ such that $e_i \rightarrow 0$ in $J$. Thus, we get a unique continuous $R$-algebra map
$$f:R[\![X_i]\!] \rightarrow A$$
satisfying $X_i \mapsto e_i \in J$ and want to show that $f$ is an isomorphism.
By design, $f \widehat{\otimes}_R \kappa$ is surjective between formal cotangent spaces, so it is surjective onto every discrete quotient of $A \widehat{\otimes}_R \kappa$ and hence is surjective (by exactness of inverse limits on the category of "pro-finite" $R$-modules). But $R$ is artinian, so $f \widehat{\otimes}_R \kappa = f \otimes_R \kappa$. It follows that $f$ is surjective (and hence is a topological quotient map). To prove that $\ker f = 0$, suppose there is a nonzero $\phi \in \ker f$. Informally, we will stare at the power series expansion of $\phi$ to find appropriate artin local test objects (with residue field $\kappa$) that violate the formal smoothness of $A$ over $R$. Carrying this out goes in 4 steps: first we show that $f$ is an isomorphism when $R = \kappa$, then we use that to $J/\overline{J^2}$ is topologically free over $R$ with $a_i$'s as a topological basis, and finally we use that to deduce that $\ker f = 0$.
Step 1: Let's consider the case $R = \kappa$, so we have
$$f:\kappa[\![X_i]\!] \twoheadrightarrow A$$
that is an isomorphism between formal cotangent spaces, and we want to show that $\ker(f) = 0$. The induced map modulo closures of squares of maximal ideals is an isomorphism since $X_i \mapsto a_i \in \mathfrak{m}_A$ where by design the $a_i$ lift a topological basis of the formal cotangent space $\mathfrak{m}_A/\overline{\mathfrak{m}_A^2}$. Hence, any $\phi \in \ker(f)$ is supported in degrees $\ge 2$. By induction on $r \ge 1$ let's show that any such $\phi$ is supported in degrees $> r$ (so $\phi$ must vanish). The case $r=1$ is settled, so we may assume $r \ge 2$ and that the result is known for $r-1$. Suppose to the contrary that $\phi$ contains a least-degree monomial term $x_{i_1}^{e_1} \cdots x_{i_d}^{e_d}$ with some $d \ge 1$ and $e_j \ge 1$.
By formal smoothness, the quotient map
$$A \twoheadrightarrow A/\overline{\mathfrak{m}_A^2} = \kappa[\![X_i]\!]/\overline{(X_i)^2} \twoheadrightarrow \kappa[X_{i_1},\dots,X_{i_d}]/(X)^2$$
(final step killing $X_i$ for $i \ne i_1, \dots, i_d$) that carries $a_i$ to $X_i$ for $i = i_j$ and kills all other $a_i$'s lifts to a continuous $\kappa$-algebra map $$A \rightarrow \kappa[X_{i_1},\dots,X_{i_d}]/(X)^{r+1}$$ whose composition with $f$ carries $X_{i_j}$ to $X_{i_j} + h_j$ where $h_j \in (X_{i_1},\dots,X_{i_d})^2$, and sends other $X_i$'s into $(X_{i_1},\dots,X_{i_d})^2$. The element $\phi$ which contains $X_{i_1}^{e_1} \cdots X_{i_d}^{e_d}$ as a least-degree nonzero monomial term cannot be killed under such a composite map, contradicting that $f(\phi)=0$.
This settles the case $R = \kappa$.
Step 2: Now we show for general artin local $R$ that the $a_i$'s constitute a topological basis of $J$ over $R$. Surjectivity of $f$ shows that the $a_i$'s topologically span $A$, and we have to show that for any relation $\sum c_i a_i = 0$ with $c_i \in R$ (the sum makes sense since $a_i \rightarrow 0$ in $A$), necessarily all $c_i$ vanish. Certainly all $c_i$ lie in $\mathfrak{m}_R$, since the $a_i$'s were chosen to lift a topological $\kappa$-basis of the formal cotangent space of $A\widehat{\otimes}_R \kappa$. Pick an index $i_0$ and consider the map
$$A \twoheadrightarrow A \widehat{\otimes}_R \kappa =
\kappa[\![X_i]\!]/\overline{(X_iX_{i'})} \twoheadrightarrow \kappa[X_{i_0}]/(X_{i_0}^2)$$
that kills $a_i$ for $i \ne i_0$ and send $a_{i_0}$ to the class of $X_{i_0}$.
Using the $R$-algebra section $s$ which kills $J$ (hence kills every $a_i$), we get an $R$-algebra map to the fiber product $R$-algebra $R \times_{\kappa} \kappa[X_{i_0}]/(X_{i_0})^2$ that is a quotient of $R[X_{i_0}]/(X_{i_0})^2$. Formal smoothness over $R$ then provides a continuous $R$-algebra lift
$F:A \rightarrow R[X_{i_0}]/(X_{i_0}^2)$ which carries every $a_i$ to $b_i X_{i_0}$ for some $b_i \in R$ (all but finitely many of which must vanish) with $b_{i_0}$ a 1-unit and all other $b_i$ in the maximal ideal of $R$.
Feeding the relation $\sum c_i a_i = 0$ in $A$ into the lift $F$ then gives $\sum c_i b_i = 0$ in $R$ (look at $X_{i_0}$-coefficients). But all $c_i$ lie in the maximal ideal, so all $c_i b_i$ lie in the square of the maximal ideal for $i \ne i_0$. Hence, since $b_{i_0}$ is a unit, we deduce that $c_{i_0}$ is in the square of the maximal ideal. But $i_0$ was arbitrary, so all $c_i$ lie in $\mathfrak{m}_R^2$.
We can now feed this conclusion back into the same calculations to see that all $c_i$ lie in $\mathfrak{m}_R^e$ for $e = 3, 4, \dots$, and hence all $c_i$ vanish.
This concludes the proof that the $a_i$'s are a topological $R$-basis of $J/\overline{J^2}$.
Step 3: The method of Step 1 used that we are over a field solely because the $a_i$'s are then a topological basis of the formal cotangent space, which is $J/\overline{J^2}$ in the case that $R$ is a field. But Step 2 proved this basis property for any artin local $R$, from which we see that the induced map
$$R[\![X_i]\!]/\overline{(X_iX_{i'})} \twoheadrightarrow A/\overline{J^2}$$
is a (topological) isomorphism. So we can repeat the method of Step 1 verbatim with $\kappa$ there now replaced with our general $R$.
QED
