Today the cloud market is restricted to few providers, which entails higher prices, vendor lock-in and lower service quality. Smart Contracts (SC) and blockchain could reshape this market since they lower costs and provide trust without resorting to intermediaries. This paradigm, named blockchain-based clouds, prevents vendor lock-in and has the potential to make market's barriers so low that anyone with idle or spare computational resources can offer cloud services. The STARCloud project systematically utilises formal methods for the static analysis and runtime control of the next generation clouds for creating support for Quality of Service (QoS). To this aim, since the state-of-the-art solutions cannot be used in this domain, this project provides novel approaches and tools, including consensus mechanisms, a domain specific language for QoS definitions and QoS formal analysis tools, and a framework for the matchmaking and negotiation of SCs.