...

We are working towards a version of CPSA with the property that whenever it successfully terminates, every possible execution is described by its output.  However, the current implementation occasionally fails to find some executions.

That is concerning - is it due to ...

We have formally specified the algorithm, but we haven't been able to prove the algorithm finds all solutions. In fact, we now have an example in the test suite that shows it misses an answer. The example is in the source distribution in tst/missing-contraction.scm. There should be two answers, but CPSA only finds one. We have a fix you can try out in 2.0.4. In src/CPSA/Lib/Strand.hs, you can change the flag useDisplacement from False to True, and CPSA will find both answers. We don't know if this fix is all one needs to ensure CPSA finds every answer. By the way, the algorithm is in doc/cpsaspec.pdf, which can be build from a source distribution of CPSA.

What is the current status of development both wrt openness and future direction?

Our highest priority is to resolve the correctness issue you just raised. As for openness, the sources are available to you. We haven't thought about other forms of openness.

 I'm wondering if you plan to add MQV or other non-trivial primitives.

I don't know what MQV is, so I can't say. Thanks for your interest, Thomas. John