The C4 project aims at building a correct-by-construction concurrent transaction-processing system.  Programmers write transactions in high-level relational notations.  The system refines high-level programs into efficient low-level multicore code with the guarantee that the generated code is strictly serializable with respect to the specification.  The refinement process benefits from a verified cross-composable library of concurrent data types.  (A concurrent data type is said to be cross-composable if not only it is linearizable but also multiple method calls on multiple instances of it can be composed to an atomic operation.)  The library supports multiple implementation techniques including Transactional Memory, Boosting and Predication.  The verification framework formalizes a unified model of composable objects that subsumes linearizability and strict serializability.  It supports verification of these conditions assuming the basic rules of logic and the semantics of basic synchronization data types.  The framework is being developed in Coq.