Random-matrix pair correlation for a specific chaotic billiard

Dirichlet Laplacian on the Bunimovich stadium or the Sinai billiard, eigenvalues $\lambda_n \to \infty$ unfolded by Weyl's law. Prove that the pair correlation converges to the GOE two-point function, or at least that the spectral form factor satisfies $K(\tau) = 2 \tau - \tau \log(1 + 2 \tau)$ for small $\tau > 0$. Answer: a proof.

A proof for one billiard or one negatively curved surface without arithmetic symmetry.