In this blog post, we'd like to share how we build formal verification and fuzzing tools, highlight some of the projects we've developed—such as Kontrol, Kasmer, and Komet — and delve into what it takes to create a tool for formal semantics. Our goal is to provide insights for teams interested in using and developing similar tools for their smart contract languages or ecosystems.