This article introduces the Spunky microkernel project recently presented at the 10th Ada Developer Room at FOSDEM 2020 [3]. The Spunky project aims for providing a kernel for the Genode OS framework written in Ada that may subsequently be transferred to SPARK to enable automated proving of fundamental kernel aspects.