Do you have a TLA+ spec of the flawed sorting algorithm ?
I am also not sure what kind of symbolic execution you are after.
The answer of Leslie Lamport refers to BDD-based symbolic model checking.
The ProB tool can be used for constraint-based symbolic execution, which in turn can be used for bounded model checking or test-case generation.
Below is an artificial example, where the ProB bounded model checker finds a counter-example (Init with ct=33554431 followed by Inc(1)) immediately by solving the corresponding constraints, but the explicit model checking with TLC reports: "Too many possible next states…"
Is this the kind of symbolic execution you are after ?
Of course, ProB’s support for TLA+ is unfortunately still limited (the TLA+ specs have to go through a typechecker, no support for user-defined recursive operators,… ); but we would be happy to try out more involved examples.
---- MODULE VerySimpleCounterWrongLargeBranching ----
lim == 2^25
Invariant1 == ct \in Int
Invariant2 == ct < lim
Init == ct \in (0 .. lim - 1)
Inc(i) == ct + i =< lim
/\ ct' = ct + i
Reset == ct = lim
/\ ct' = 0
Next == \/ \E i \in (1 .. 1000) : Inc(i)
The config file is: