I understand what you're saying, but I think that it's possible to approximate model checking with property testing, by defining your model's invariants as properties, and then generating a list of symbolic commands to run against your model.

Like you said, you won't be testing all of the possible inputs, but it can still be a very effective way to detect the kinds of bugs that would otherwise be difficult to discover with more traditional testing methods.

Here's an example of what I'm talking about: http://propertesting.com/book_stateful_properties.html

Randomized testing is very good, but it is so fundamentally different from model checking that it's not an approximation in any meaningful sense (except in the sense that both are automated methods that can find bugs). Again, even an explicit-state model checker can quickly check infinite executions. An interesting hybrid between the two is concolic testing (see https://youtu.be/MDzRV3OQtyQ which quickly shows the difference in power between concolic testing and randomized testing). Concolic testing is one of the most promising areas in formal verification these days.

Also, the use of the term "non-formal" in the article you linked is incorrect. If it runs on the computer it is, by definition, formal. The author meant "sound" or "exhaustive" (although, while all model checkers are exhaustive, many -- like the one in this article -- don't actually try each input; they're exhaustiveness implies soundness, not a particular brute-force algorithm. How well they can actually beat brute force is, however, another matter...).

BTW, it is possible to use the TLC model checker for randomized tests of TLA+ specifications in a way similar to randomized testing of "stateful properties", as checking random walks of the state graph.

Thank you for clarifying what you mean!

I was using the same terminlogy as the article, and treating my property tests as informal forms of model checking due to their being unsound, but I can see how that isn't exactly correct.