Zero-knowledge proofs are two-party interactive protocols where one party (the prover) convinces the other one (the verifier) that it knows some secret value, without leaking anything about this secret. ZK proofs have a vast applicability in the domain of cryptography, stemming from the fact that they can be used to force potentially malicious parties to abide by the rules of a protocol, without forcing them to reveal their secrets. In this talk I will a give an intuitive introduction to interactive ZK proofs and describe in more detail a class of three-round ZK proofs, known as Sigma-protocols. I will show how Sigma-protocols can be formalized as probabilistic programs in the CertiCrypt framework—built on top of the Coq proof assistant—and how mechanized programming language techniques can be used to formally prove that a protocol is complete (a honest prover always convinces a verifier), sound (a dishonest prover can only convince a verifier with negligible probability) and perfect zero-knowledge (a verifier does not gain any secret information from participating in the protocol). I will also show how a large class of ZK proofs can be seen as instances of a generic Sigma-protocol, for which soundness, completeness and zero-knowledge can be established once and for all. I will conclude by describing a means of combining ZK proofs to obtain proofs of more complex formulae using the AND and OR Boolean operators.