Carbon credits purchased in the voluntary carbon market allow unavoidable emissions, such as international flights for essential travel, to be offset by an equivalent climate benefit, such as avoiding emissions from tropical deforestation. However, many concerns regarding the credibility of these offsetting claims have been raised. Moreover, the credit market is manual, therefore inefficient and unscalable, and non-fungible, therefore illiquid. To address these issues, we propose an efficient digital methodology that combines remote sensing data, modern econometric techniques, and on-chain certification and trading to create a new digital carbon asset (the PACT stablecoin) against which carbon offsetting claims can be transparently verified. PACT stablecoins are produced as outputs from a reproducible computational pipeline for estimating the climate benefits of carbon offset projects that not only quantifies the CO2 emissions involved, but also allows for similar credits to be pooled based on their co-benefits such as biodiversity and jurisdictional attributes, increasing liquidity through fungibility within pools. We implement and evaluate the PACT carbon stablecoin on the Tezos blockchain, which is designed to facilitate low-cost transactions while minimizing environmental impact. Our implementation includes a contract for a registry for tracking issuance, ownership, and retirement of credits, and a custodian contract to bridge on-chain and off-chain transactions. Our work brings scale and trust to the voluntary carbon market by providing a transparent, scalable, and efficient framework for high-integrity carbon credit transactions.

Poorly specified smart contracts can be vulnerable to attacks on faulty design. Formal methods are currently unable to address these vulnerabilities because they are not vulnerabilities of incorrect code, but of incorrect specification. We are thus in need of a paradigm shift in how we specify and verify smart contracts which allows for a rigorous and accurate notion of a contract specification’s correctness. We submit that correctness includes appropriate cryptoeconomic behaviors, which are generally out of scope of a contract’s specification. We advocate for an approach to contract specification consisting of contract axiomatization and metaspecification, and illustrate with an example.

Tokenized carbon credits are of growing relevance to voluntary carbon markets, but because tokenized carbon credits are typically NFTs, they suffer from low liquidity and high price volatility on-chain. Current solutions pool carbon credits to enable greater liquidity, but are incomplete. We present a novel pooling mechanism which we call a structured pool, which addresses issues with current pooling techniques.