The partition function on the three-sphere of ABJM theory contains non-perturbative corrections which correspond to membrane instantons in M-theory. These corrections can be studied in the Fermi gas approach to the partition function, and they are encoded in a system of integral equations of the TBA type. We study a semiclassical or WKB expansion of this TBA system in the ABJM coupling k, which corresponds to the strong coupling expansion of the type IIA string. This allows us to study membrane instanton corrections in M-theory at high order in the WKB expansion. Using these WKB results, we verify the conjectures for the form of the one-instanton correction at finite k proposed recently by Hatsuda, Moriyama and Okuyama (HMO), which are in turn based on a conjectural cancellation of divergences between worldsheet instantons and membrane instantons. The HMO cancellation mechanism is important since it shows in a precise, quantitative way, that the perturbative genus expansion is radically insufficient at strong coupling, and that non-perturbative membrane effects are essential to make sense of the theory. We propose analytic expressions in k for the full two-membrane instanton correction and for higher-order non-perturbative terms, which pass many consistency checks and provide further evidence for the HMO mechanism.