Add a formal HAL specification consisting of: -defined and undefined behavior -test descriptions -enable doxygen for MPU