🚧 WORK IN PROGRESS 🚧

Overview

This repository contains wallet implementations for the Cardano blockchain that are formally verified to some degree. The implementations are Haskell packages, but generated using agda2hs, with proofs in Agda.

Contents

This repository is strucured as follows:

• flake.nix — Nix flake for a development shell with relevant Haskell and Agda tools in scope.
• lib/
  • customer-deposit-wallet-pure/ — Specification and implementation of a pure Deposit Wallet.
  • cardano-wallet-read/ — Data types that correspond to the Cardano Ledger specification, implemented via the cardano-ledger packages.

Each of the packages in the lib/ directory may contain the following subdirectories:

• agda/ — Haskell-in-Agda code with some proofs.
• haskell/ — Haskell code that corresponds to the code in agda/. Most source code files are autogenerated from the agda/ directory using agda2hs, but not all. This code is checked into the repository, so that downstream projects do not need the Agda compiler.

QuickStart

Prerequisites:

• Nix package manager.

How to build:

nix develop
just haskell
just build

How to run tests:

• There are no unit tests for customer-deposit-wallet-pure — only compiler-checked proofs. 😏
• To run the unit tests for cardano-wallet-read, use just test.

How to run:

• N/A. This project is a Haskell package. For an exectuable wallet, see the cardano-wallet project.

Contributors

See CONTRIBUTING.md.

Roadmap

• Completion of implementation.
• Completion of proofs.