Third-Party Applications

The following projects use cvc5:

• Atelier B: An industrial tool enabling the operational use of the B Method to develop provably defect-free software. CVC4 is one of the backend provers.

• Boogie: A program verifier using the Boogie intermediate verification language. Supports CVC4 as a backend.

• CIVL: A symbolic execution-based model checker for a dialect of C supporting concurrency. CVC4 is one of the backend provers.

• Certora: Certora provides security analysis tools for Smart Contracts. The Certora Prover is capable of checking at compile-time that all executions of a Smart Contract fulfill a set of security rules. CVC4 is one of the backend provers.

• CoSA: An SMT-based symbolic model checker for hardware design.

• GPUVerify: A tool for formal static analysis of GPU kernels written in OpenCL and CUDA. It can prove that kernels are free from defects such as data races and barrier divergence. It is built on top of the Boogie verification engine, using CVC4 as one of the available theorem provers.

• Inductor: A theorem prover for entailments between inductive definitions in first order and separation logics.

• Inox (formerly Leon): A solver for higher-order functional programs. Supports CVC4 as a backend.

• Isabelle (Sledgehammer): Isabelle is a generic proof assistant. Sledgehammer applies automated reasoning tools (including CVC4) to solve Isabelle subgoals.

• Kind 2: A multi-engine SMT-based automatic model checker for safety properties of Lustre programs. It supports cvc5 as a backend solver. It also uses cvc5 proof production capabilities to generate proofs for model properties that Kind 2 claims to be valid.

• Maude: A system supporting equational and rewriting logic specification and programming. Uses CVC4 as a backend.

• Pysmt: A generic python interface for SMT solving. Supports CVC4 as a backend.

• QMaxUSE: QMaxUSE is a query-based verification tool for verifying UML class diagrams with OCL invariants. It supports a query language and concurrent verification. QMaxUSE uses cvc5 as one of its backend solvers.

• Rosette: A solver-aided programming language that extends Racket with language constructs for program synthesis and verification. Supports CVC4 as a backend solver.

• SMTCoq: A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers.

• SPARK: SPARK is a verification paradigm for a subset of the Ada programming language. It uses CVC4 as the default backend for solving verification conditions.

• Solc-Verify: An extended version of the Solidity compiler (v0.5.17) able to perform automated formal verification on Solidity smart contracts using specification annotations and modular program verification. CVC4 is one of the backend provers.

• Solidity’s SMTChecker: A built-in formal verification module in the Solidity Compiler. CVC4 is one of the backend provers.

• TRLC (using PyVCG): TRLC is a text-based requirement language used at BMW, which includes user-defined checks that may raise run-time errors (like division by zero). TRLC includes a linter that uses cvc5 to prove absence of run-time errors for these user-defined checks.

• TorXakis: A model-based testing framework.

• Why3: A platform for deductive program verification. Uses CVC4 as an external prover.

• Zelkova: Zelkova uses an encoding into the SMT theory of strings to check the security of access policies on Amazon Web Services.

If you use cvc5, please contact us and we’ll add your application here!