Ivan Smith's formality conjecture for hyperkähler Fukaya categories

Let $(\mathrm{X},\mathrm{I},\mathrm{J},\mathrm{K},g)$ be a hyperkähler manifold, and let $\mathfrak{L}$ be a collection of compact spin $\mathrm{I}$-holomorphic Lagrangian submanifolds with clean pairwise intersections. Let $\widehat{\mathcal{A}}_\mathfrak{L}$ be the associated $\mathrm{A}_\infty$-category. Ivan Smith's formality conjecture. The $\mathrm{A}_\infty$-category $\widehat{\mathcal{A}}_\mathfrak{L}$ is formal. This is the Fukaya-side analogue of the paper's de Rham formality theorem; intrinsic formality is known for a particular Slodowy-slice example, but the stated general conjecture remains open.