Imandra [1] has an excellent literate programming walkthrough that hits on the same issues and plugs the holes one by one using formal methods, ultimately proving merge sort correct.

[1] https://docs.imandra.ai/imandra-docs/notebooks/verifying-mer...