have any audit firms done model checking on smart contracts?

I’m a research engineer passionate about high-impact technology. My interests lie at the intersection of mathematics, computer science, and philosophy

Cofounder of 0xMacro.com • Author of LearnEVM.com • Love to help with no strings attached

By model checking i mean the process of verifying the correctness of a model of a system. It requires a finite state model (you can model smart contracts as FSM with satisfiable state transitions functions), and then commonly uses linear temporal logics to check correctness.

Actually this is a good resource https://www.cs.cmu.edu/~aldrich/courses/413/slides/28-model-checking.pdf

By model checks do you mean data model design, smart contract architecture, something else?