Our formalisation of Schutz’ Independent Axioms for Minkowski Spacetime is now available in Isabelle’s Archive of Formal Proof. More information and the theories are available here.