Software that can produce independently checkable evidence for the correctness
of its output has received recent attention for use in certifying compilers and
proofcarrying code. CVC (“a Cooperating Validity Checker) is a proof-producing
validity checker for a decidable fragment of ﬁrst-order logic enriched with
background theories. This paper describes how proofs of valid formulas are
produced from the decision procedure for linear real arithmetic implemented in
CVC. It is shown how extensions to LF which support proof rules schematic in an
arity (“elliptical” rules) are very convenient for this purpose.