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

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

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

Ah, so applying tools like Certora, Halmos, Echidna? Or more generalized formal verification such as Isabelle, Coq, Alloy?

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