Alloy is a brute force model checker (for rather small models).
Is that the state of the art for formal methods? How do you think of formally verifying systems with floating points calculations, with randomness, with databases and external environments?
> Is that the state of the art for formal methods?
I think the state of the art is quite broad as there are many tools.
Model checking is, in my estimation, the most useful for industry programmers today. It doesn't require as much training to use as automated theorem proving, it doesn't provide the guarantees that mathematical induction and proof do; but you get far more for your buck than from testing alone.
However model checkers are very flexible because the language they use, math, is also very flexible. TLA+ has been used to find errors in the Xbox 360 memory controller before it went to launch as well as in Amazon's S3 [0] -- errors so complex that it would have been highly improbable that a human would detect them and the result of finding those errors and solving them saved real businesses a lot of money.
It comes down to your ability to pick good levels of abstraction. You can start with a very high level specification that admits no details about how the file system works or the kernel syscalls involved and still get value out of it. If those details _do_ matter there's a strategy called refinement where you can create another specification that is more specialized and write an expression that implies if the refined specification holds then the original specification does as well.
Tools for randomness and numerical methods exist and depending on your needs you may want to look at other tools than just a model checker. TLA+, for example, isn't good at modelling "amounts" as it creates a rather large state space quickly; so users tend to create abstractions to represent these things with a finite number of states.
Is that the state of the art for formal methods? How do you think of formally verifying systems with floating points calculations, with randomness, with databases and external environments?