Architecting IoT systems able to guarantee Quality of Service (QoS) levels can be a challenging task due to the inherent uncertainties (induced by changes in e.g., energy availability, network traffic) that they are subject to. Existing work has shown that machine learning (ML) techniques can be effectively used at run time for selecting self-adaptation patterns that can help maintain adequate QoS levels. However, this class of approach suffers from learning bias, which induces accuracy problems that might lead to sub-optimal (or even unfeasible) adaptations in some situations. To overcome this limitation, we propose an approach for proactive self-adaptation which combines ML and formal quantitative verification (probabilistic model checking). In our approach, ML is tasked with selecting the best adaptation pattern for a given scenario, and quantitative verification checks the feasibility of the adaptation decision, preventing the execution of unfeasible adaptations and providing feedback to the ML engine which helps to achieve faster convergence towards optimal decisions. The results of our evaluation show that our approach is able to produce better decisions than ML and quantitative verification used in isolation.