The coq-uplc library provides a Coq-based implementation of the Cardano CEK machine—the virtual
machine responsible for evaluating UPLC programs (validators), which serve as the on-chain
components of Cardano smart contracts.
Cardano validators, the backbone of its smart contract ecosystem, can be written in various high-level languages and dialects, such as:
- Plutus, Plutarch, Aiken, Marlowe, Helios, OpShin, and plu-ts.
To function on the Cardano blockchain, every validator must be compiled into UPLC (Untyped Plutus Core). This is crucial for Cardano nodes to evaluate and authorize transactions associated with these validators.
Validators ensure the security of Cardano's protocols, safeguarding the transmission and storage of funds. However, vulnerabilities in their implementation can lead to catastrophic outcomes, such as funds being stolen, lost, or permanently locked.
Coq is a state-of-the-art interactive theorem prover renowned for its reliability and utility in critical domains, including compiler construction. Built on first-order mathematical logic, type theory, and the calculus of constructions, Coq is well-suited for defining and proving properties of validator programs.
- Formal Verification: ensures the mathematical soundness of validators.
- Automation with Tactics: simplifies proof scripts, aiding in proof maintenance and enabling efficient updates to existing validators.
Using Coq enhances confidence in the correctness of validator implementations, reducing risks in Cardano's ecosystem.
- Install Nix and enable Nix flakes.
- In the project root, run:
This starts a development shell.
make shell
- Build the library with:
make build
- Install Opam and initialize it:
opam init
- Install the required dependencies:
opam install coq dune
- Build the library by running:
opam exec -- dune build
Under construction...