\documentclass{article}
\usepackage{luamml-pdf}

\RegisterFamilyMapping\symsymbols{oms}
\RegisterFamilyMapping\symletters{oml}
\RegisterFamilyMapping\symlargesymbols{omx}

\ExplSyntaxOn
\cs_set_eq:NN \WriteoutFormula \luamml_pdf_write:
\NewDocumentCommand\AnnotateFormula{ o m m }{%
  \IfValueTF{#1}{%
    \luamml_annotate:nen{#1}%
  }{
    \luamml_annotate:en
  }{#2}{#3}
}
\ExplSyntaxOff

\protected\edef\models{\AnnotateFormula{%
    nucleus = true, core = {[0] = 'mi', '\noexpand\string\noexpand\u{22a7}'},
  }{\unexpanded\expandafter{\models}}}

\begin{document}
\[
  \emptyset\models((p\Rightarrow q)\Rightarrow(q\Rightarrow r))\Rightarrow (p\Rightarrow (q\Rightarrow r))
  \WriteoutFormula
\]

%\begin{align}
%  abc&=def & e^{\mathrm{i}\pi}&=-1\\
%  \Big(1+2&=3\Big)\\
%  &4\\
%  5
%\end{align}

Es gilt $\sin(x)-\sin(x+2\pi)=0\WriteoutFormula$.
\end{document}