The soundness of invariant admissibility, ownership, and claims is described in the CAV paper.
The 2009 tech report gives the operational semantics of a small language, and describes the reduction theorem that allows us to pretend that scheduler boundaries occur only before atomic actions (with a suitable interpretation of what assertions within threads
mean).
The semantics we use for sequential C is essentially given in the translation to Boogie, which you can find in the source code but has not been written about separately.
Sabine Schmaltz <sabine@wjpserver.cs.unisaarland.de> is working on a more careful operational semantics and soundness proof; you might want to contact her directly.
