Formal verification in cryptography I have seen in some places that people use formal verification and/or computer-aided verification for cryptography (tools like ProVerif, CryptoVerif, etc.). 

How do these approaches work?
Disclaimer: I use Coq on daily basis...




  I have seen in some places that people use formal verification and/or computer-aided verification for cryptography.


To my knowledge, there aren't that many places that do such a thing.



First, let's define our concepts:

Formal Verification: The act of proving the correctness of algorithms with respect to a certain formal specification or property, using formal methods of mathematics.

Computer-assisted proof: A proof that has been at least partially generated by computer.

Some examples (in cryptography):


Verification of a Cryptographic Primitive: SHA-256 (paper)
Formal certification of game-based cryptographic proofs (PHD)


And some reading:


A gentle introduction to formal verification of computer systems by abstract interpretation (paper)
A Foundational Proof Framework for Cryptography (PHD)
Computer Verification in Cryptography (paper)
Probabilistic Relational Verification for Cryptographic Implementations (paper)




How does it work?

In formal methods (whatever the domain) there are two approaches:


Specification $\rightarrow$ Software
Specification $\wedge$ Software $\rightarrow$ Prove the software's correctness.


In most cases, the first method is the one used. Why? Because it is easier to start with a formal specification and then, incrementally, through proven steps, eventually get to the software (which is therefore proven). As an example, this certified compiler:


For example in the Method B, the process is the following:
$$DEFINE\ /\ SPECIFY \rightarrow PROVE \rightarrow  REFINE \rightarrow PROVE \rightarrow  \ldots \rightarrow IMPLEMENT$$

Formal verification uses the Hoare logic, a set of rules that allows us to reason about programs. It is based on sequent calculus and natural deduction. It relies on the Hoare triple:
$$\{P\}\ C\ \{Q\}$$
When the precondition $\{P\}$ is met, the execution of the command $C$ establish the postcondition $\{Q\}$. If the command $C$ goes from a state $s$ to a state $s'$.
$$C: s \rightarrow s'$$
Then you will have to prove:
$$\forall\ s\ s', P[s] \implies C : s \rightarrow s' \implies Q[s']$$
But we prefer the Hoare triple notation (lighter).

As an example, this is the rule for $SKIP$ (aka do nothing):
$$\frac{}{\{P\}\ SKIP\ \{P\}}$$

And this is the rule for the sequence :
$$\frac{\{P\}\ C_1\ \{Q\}\ \ \ \ \ \ \ \{Q\}\ C_2\ \{R\}}{\{P\}\ C_1 ; C_2\ \{R\}}$$
This notation is read as :
"If $\{P\}\ C_1\ \{Q\}$ (is $\text{True}$) and if $\{Q\}\ C_2\ \{R\}$, I can infer $\{P\}\ C_1 ; C_2\ \{R\}$.

A proof is therefore built from bottom to top : if you want to prove $\{P\}\ C_1 ; C_2\ \{R\}$, you will need to prove there is $Q$ such as $\{P\}\ C_1\ \{Q\}$ and $\{Q\}\ C_2\ \{R\}$.

Some readings on Hoare logic:


Background reading on Hoare logic (course)
Handout C2: Reasoning About Code (Hoare Logic) (course)
Software Foundation (self study course, highly recommended if you want to get into the domain).




The tools

In formal methods, there are two kinds of tools:


the fully-automated prover
the proof assistants


The first are mainly based on SMT (satisfiability modulo theories) such as Atelier B and Alt-Ergo. 

The second ones are based on pure logic. You provide it with lemmas (helping theorems), and this will make sure that every step you do in your proof is right. It is a very thorough process, quite slow. But at the end you know how your proof works and that it is correct because you did not miss a hypothesis. The process, which can be frustrating, will make sure that the proof works.
The main proof assistants are the following: Coq, 
Isabelle, Agda, Fstar and HOL.

The tools you mentioned (ProVerif, CryptoVerif) are not dedicated to cryptographic primitives, but protocol verification. I do not know them, so I will not comment. Other tools on the same subject do exist. For example:


CertiCrypt
EasyCrypt (tutorial)


And yes, they are based on Coq.

In C, in order to be able to verify your code matches your specification (such as what has been done for $\text{SHA-}256$), one need to extract the semantic from the code. This could be done using the Verifiable Tool Chain or Why3. The first one will provide you a Coq file from which you will be able to start your proofs. The second one, given C ASCL instrumented code, will use frama-c and try to prove the properties with the SMT provers named above. On failure, it generates goals and asks you to prove them with Coq.



In Cryptography (and Mathematics)

I already mentioned the idea of proving protocols (cf EasyCrypt et al.), for cryptographic proofs, the idea is basically the same. Specify using logic properties.

Coq example (trivial to prove by hand for a undergrad student):
$$\forall\ f g, f \text{ is injective} \implies g \text{ is injective} \implies g \circ f \text{ is injective}$$

Require Import Coq.Sets.Image.

Theorem injective_trans:
forall A B C (f: A -&gt; B) (g:B -&gt; C) (h:A -&gt; C),
(forall x, h x = g (f x)) -&gt; injective A B f -&gt; injective B C g -&gt; injective A C h.
Proof.
intros A B C f g h H_h_equal_g_f H_f_injective H_g_injective.
unfold injective in *.
intros x y H_h_x_y.
apply H_f_injective.
apply H_g_injective.
rewrite &lt;- H_h_equal_g_f.
rewrite &lt;- H_h_equal_g_f.
apply H_h_x_y.
Qed.


Here is a list of famous proven theorem in Coq.



Final words

Security bounds in Keccak has been proven with the aid of a computer. But their process was different: they exhaustively generated the trails and showed the properties. Thus it was computer aided, but not verified.

And finally, a recent paper from FSE 2016: Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC

As SEJPM pointed out, this paper is also another kind of approach (more game based). They created an analyzer that generated a cipher scheme that satisfied the AE scheme. However, I don't know whether they have proven their properties by hand or used a proof assistant (which might be possible given that they used Ocaml to code their analyzer). 



You might also be interested in the course Gilles Barthe (EasyCrypt team) has done here.

I do not know if my answer has been helpful. I know it is not mainly focused on cryptography, but I hope it will give you a some idea of how things work.