---
name: "cvc4"
section: "5"
platform: "linux"
package: "cvc4"
version: "1.8-3"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/cvc4/5"
---

# cvc4(5)

the native input language for CVC4

## NAME

cvc4 - the native input language for CVC4

## DESCRIPTION

**cvc4** is an automated theorem prover for first-order formulas with respect to background theories of interest.

## HISTORY

## SEE ALSO

[**cvc4**(1)](/cvc4/1.md), [**libcvc4**(3)](/libcvc4/3.md), [**libcvc4parser**(3)](/libcvc4parser/3.md)

Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4.  It is maintained at **http://cvc4.cs.stanford.edu/wiki/**.