What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator? In lambda calculus or in combinatory logic we formally define reduction/expansion rules for terms (and in their typed variants reductions must preserve the type). Then we can talk about properties of such systems, in particular about the normalization property or confluence.

How could one formally define reductions for the call/cc (call with the current continuation) operator in terms of a rewrite system?

The semantics of the operator allows to abandon the current evaluation context and return to the point where the continuation was captured, effectively allowing the evaluation state to become explicit.

I'd be interested in such a definition that'd allow to formally talk about  confluence of such a system (and showing it doesn't hold, as the behavior of the operator depends on the evaluation order).
The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of reductions, but clarify the presentation in my opinion. 
Let's assume your language is given by
the following grammar.
$$
\newcommand{\PROGRAM}[1]{\mathsf{#1}}
\newcommand{\FV}[1]{\mathsf{fv}(#1)}
\newcommand{\DOM}[1]{\mathsf{dom}(#1)}
\newcommand{\VERTICAL}{\;  \mid\hspace{-3.0pt}\mid \; }
\newcommand{\CALLCC}{\PROGRAM{callcc}}
\newcommand{\CONT}[1]{\mathsf{Cont}(#1)}
\newcommand{\THROW}{\PROGRAM{throw}}
\newcommand{\infer}[2]{\frac{\displaystyle{ #1 }}{\displaystyle{ #2 }}}
\newcommand{\ZEROPREMISERULE}[1]{\infer{-}{#1}}
\newcommand{\FS}{\rightarrow}
\newcommand{\RED}{\rightarrow}
\newcommand{\ONEPREMISERULE}[2]{\infer{#1}{#2}}
\newcommand{\TYPES}[3]{#1 \vdash #2 : #3}
\newcommand{\TWOPREMISERULE}[3]{\infer{#1 \quad #2}{#3}}
   M ::= x \VERTICAL \lambda x.M \VERTICAL MM \VERTICAL ... \VERTICAL \CALLCC \VERTICAL \THROW
$$
Here $\CALLCC$ and $\THROW$ are seen as constants although we could also have defined them in different ways.
Let us denote by $\FV{M}$ the free variables of the program $M$.
Types could be something like this:
$$
        \alpha\
                ::=\
        \alpha \FS\alpha
\VERTICAL \PROGRAM{Int} \VERTICAL
        ...
                \VERTICAL
        \CONT{\alpha}
$$
Here $\CONT{\alpha}$ is the type of continuations with final answer
type $\alpha$.
The constants $\CALLCC$ and $\THROW$ are values and have the following types.
$$
        \ZEROPREMISERULE
        {
          \TYPES{\Gamma}{\CALLCC}{(\CONT{\alpha} \FS \alpha) \FS \alpha}
        }
                \qquad
        \ZEROPREMISERULE
 {
                \TYPES{\Gamma}{\THROW}{\CONT{\alpha} \FS \alpha \FS \beta}
        }
$$
Depending on your use-case, the type variables may be quantified.
Reductions are defined with the help of configurations. 
A configuration is a pair $(M, \sigma)$ such that $M$ is a
program and $\sigma$, the continuation map, ranged over by
$\sigma, ...$, maps each $k \in \FV{M}$ of type $\CONT{\alpha}$ to an appropriately typed program.
Then
reductions are of the form $(M, \sigma) \RED (N,                                                             
\sigma')$. For  call-by-value, the reductions are generated as usual, with the following additions for $\CALLCC$
and $\THROW$.
$$
        \ONEPREMISERULE
        {
                k, x\ \text{fresh}
        }
        {
                (E[\CALLCC\ V], \sigma) \RED (E[V\;k], \sigma \cdot k \mapsto \lambda x.E[x])
        }
                \quad
        \ONEPREMISERULE
        {
                \sigma(k) = M
        }
        {
                (E[\THROW\ k\ V], \sigma) \RED (MV, \sigma)
        }
$$
Here $V$ over ranges over values, and
$E[\cdot]$ over the usual call-by-value reduction contexts. The two new constants give rise to the following evaluation contexts: $\CALLCC\ E[\cdot]$, $\THROW\ E[\cdot]\ M$
and $\THROW\ V\ E[\cdot]$.

Note that (1) does not use continuation maps to define the CBV semantics of $\CALLCC$
 and $\THROW$. Instead a run-time value is introoduced. The two approaches are equivalent.

As to evaluation order, $\CALLCC$ enriches the power of contexts and can distinguish  programs by application that are
  indistinguishable in the absence of continuations: 

$$
  \newcommand{\ARGFC}{\PROGRAM{argfc}}
  \ARGFC  = \CALLCC\ \lambda k.(\THROW\ {k}\ {\lambda
  x.(\THROW\ {k}\ {\lambda y.x}}))
  $$

This is the classic example of calling a function once, but
  returning twice. e.g. in
  $$
  (\lambda x.(x\; 1);(x\; 2))\ \ARGFC = 1
  $$
  and
  $$
  (\lambda x.\lambda y.(x\; 1);(y\; 2))\ \ARGFC\ \ARGFC = 2
  $$

with $M;N$ being the sequential composition of $M$ and $N$, binding
more tightly than $\lambda$-abstraction.  The reason is that
continuations carry information about contexts that may be returned
(jumped) to later.




J. G. Riecke, H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other (Postscript file).
R. Harper, B. F. Duba, D. MacQueen, Typing First-Class Continuations in ML.
H. Thielecke, Continuations, functions and jumps.