Siemens evaluated and deployed ProB during the European FP7 project "Deploy".  Their conclusions can be found in the Deploy Deliverable D41.  Siemens describes the first experiments as follows:

In order to evaluate the feasibility of using ProB for checking the topology properties, Siemens sent the STUPS team at the University of Düsseldorf the models for the San Juan case study on the 8th of July 2008. There were 23,000 lines of B spread over 79 files, two of which were to be analysed: a simpler model and a hard model. It then took STUPS a while to understand the models and get them through the new parser, whose development was being finalised at that time.

ProB was able to analyze the simple model right away:

On 14th November 2008 STUPS were able to animate and analyze the first model. This uncovered one error in the assertions.

ProB had to be improved in order to analyze the hard model.  The improvements are not specific to this problem and therefore will benefit all users of ProB.

On the 8th of December 2008 STUPS were finally able to animate and validate the complicated model. This revealed four errors. Note that the STUPS team were not told about the presence of errors in the models (they were not even hinted at by Siemens), and initially STUPS believed that there was still a bug in ProB. In fact, the errors were genuine and they were exactly the same errors that Siemens had uncovered themselves by manual inspection.

This was a great success for ProB, especially since this was a real industrial problem.  Using ProB meant real savings for Siemens.  Here is the analysis that shows how much time (and therefore money) was saved:

The manual inspection of the properties took Siemens several weeks (about a man month of effort). Checking the properties took 4.15 seconds, and checking the assertions took 1017.7 seconds (i.e., roughly 17 minutes) using ProB 1.3.0.

Ever since this study has been released, performance tuning has been continued.  With the current version of ProB, assertion checking for the above problem takes less than one minute.