# Proof Production

cvc5 produces proofs in a proof calculus that faithfully reflects its reasoning. The calculus is called the Cooperating Proof Calculus (CPC). cvc5 supports retrieving a proof object via the API (see how these objects are defined in C++, C, Java, Base Python).

## Proof Rules

A comprehensive description of the **proof rules** of the Cooperating Proof
Calculus can be found here:

**Java API**enum ProofRule

enum ProofRewriteRule

### Proof Formats

Optionally, cvc5 allows to convert and output its internal proofs into the following external formats.

Note that the DOT format is only meant for visualization.