We present, for the first time, an operational semantics and a type system for a C++-like object-oriented language with both shared and repeated multiple inheritance, together with a machine-checked proof of type safety. The formalization uncovered several subtle ambiguities in C++, which C++ compilers resolve by ad-hoc means or which even result in uncontrolled run-time errors. The semantics is formalized in Isabelle/HOL.