There have been several efforts to express the BPEL semantics in a formal language – on both the previous and the current version.

Most of that work is focused on proving certain properties; an approach where a formal system – in this case, a process description – is transformed into a mathematical model. On this model, certain properties of interest may be examined, for example the reachability of activities. A property of the mathematical model may then be proven to be a property of the original system.

Read more