The main goal of this talk is to introduce my research to the FSA group and discuss possibilities and opportunities on how this research can be combined with model checking in general and with mCRL2 in particular in the context of the recently accepted TOP project AVVA (Accelerated Verification and Verified Acceleration). I will present my programming system Many-Core Levels, the principles behind it, and how it exposes a methodology to programmers that we call “Stepwise-refinement for performance”. Many-core hardware is targeted specifically at obtaining high performance. However, obtaining high performance is challenging because hardware-specific details have to be taken into account. In our system, programmers can define and choose their own level of abstraction: higher levels for readability and portability, and user-defined lower levels to incorportate more hardware-specific details to obtain higher performance.