Can an individual tester of commercial applications reasonably hope to do automated model-based testing with free and open source software tools?

My answer is "Yes, with some caveats".

The primary challenges of applications level testers (as distinguished from unit testers) are:
   1. Not enough time
   2. Vague and ambiguous specs
   3. Demands for productivity, in tests executed or bugs found

I argue that, with today's tools, available for $0, one can "Make a model, run the model". And do it quickly, on Day 1. So, the modelmaking activity serves to disambiguate the specification situation, and does not consume precious calendar time in the process ("Partial models are OK") . A model is not an application, though. To get something valuable (say, test cases) out of it, the model has to be fixed to generate properly formatted strings that can be consumed by the Application Under Test.

I offered: a rationale for model based testing in general; one approach on how to slice up an application's state space, and why Alloy was suitable for the task (It's relational, extensible, formal, bounded). Details on how to get the Alloy model to emit nicely formatted test cases I had to be vague on, because I'm still working out exactly how to best present such to an audience of professional testers. I have done similar work with Prolog. Prolog makes it obvious that you are making a parser/FSM, and you can see clearly where to build up your test case string as you imagine the Prolog code being traversed. Add a pseudo RNG to the domain definition, append the proper framing text, and you have test cases. In Alloy, the analogous mission is described  in the "exampleUsingTheCompiler"; this is a bit too arcane for workaday testers, in my opinion.

I was also honest: even if you made a model that generated 10000 test cases on day one, your productivity would still be gated by other factors, e.g. developing test harnesses, test frameworks, test oracles, maintaining the application's runtime environment, etc. The Eclipse toolset offers some helpful structure here, but it remains a tester's responsibility to actually run the tests and judge their outcomes. The model does not help this effort.

I judge the reception of my message to be mixed. Eclipse is used by coders more than modelers and testers, I know. I got a couple of nice remarks afterward, tho, and it was gratifying to see, in Ivar Jacobson's keynote later in the day, a pitch for incremental formal system development--matches nicely with Alloy modelbuilding practice.