Hey everyone,
I’d like to propose a discussion around the practical use of formal verification in everyday smart contract development. We often talk about correctness, security, and economic guarantees at a high level, but much less about how teams actually integrate formal methods into real workflows without slowing everything to a crawl.
In theory, formal verification sounds like the ideal solution to many classes of bugs. In practice, it often feels expensive, hard to maintain, and disconnected from how contracts evolve over time. I’m curious which tools people here have actually used in production, not just in research or audits. Are there verification approaches that work well for smaller, composable components rather than entire systems?
It would also be interesting to hear how people decide what is “worth” verifying. Do you focus only on core invariants and fund-holding logic, or do you try to cover governance and edge cases as well? How do you handle upgrades without invalidating previous proofs?
This isn’t about arguing that every contract needs full formal proofs. Rather, it’s about sharing experiences on where formal methods genuinely add value today, where they fall short, and how they can coexist with testing, audits, and iterative development in a fast-moving ecosystem like UNIT0.