 As well as offering these semantic models for counterfactuals, in the book Lewis offers an axiomatisation of the counterfactual logic he prefers (see Table 6 in Section 3.3 of the entry  logic of conditionals),  as well as axiomatisations for several other logics that make different choices about some of the assumptions we’ve discussed here. And he has proofs that these axiomatisations are sound and complete with respect to the described semantics.