Today I have finally been getting around to putting my attempted formalazations of Meillassoux's argument to contingency (HERE and HERE) in a Fitch style proof system, and I realized I made one big mistake in the second post.
The argument to dialetheism is invalid.
Yes there is a contradiction between (~<>K~<>R) and (~<>K~<>R). But all that entails is that Meillassoux rejects that it is not possible to know the possibility of his sentences. By double negation elimination, that means it is possible to know that R is possible. But this is his whole conclusion with respect to any sentence and it's negation.
This makes me very happy, because by the principle of charity it means that it's more likely that I got the arguments correct.