The project combines Formal Methods techniques to develop provably correct protocols for Decentralized Finance, with applications to circular economy. Our first objective is a formal, executable model of decentralized protocols, and a theoretical study of their properties. Based on this model, the second objective is a toolkit to detect potential flaws in decentralized protocols before deployment. We validate our theory and analysis toolkit through a real-world circular economy use case