Skip to main content

Translation Certification for Smart Contracts (Extended Abstract)

#plutus#smartcontract

Compiler correctness is an old problem that has received renewed interest in the context of smart contracts — that is, compiled code on public blockchains, such as Ethereum or Cardano, that often controls significant amounts of financial assets and can no longer be updated once it is committed to the blockchain. This paper discusses the design and implementation of a certifying compiler for the Plutus smart contract system using the Coq proof assistant.

Full paper

View/download PDF

Related papers

Partner with research

Investing in and contributing to Input Output Research means supporting one of the most rigorous and peer-reviewed blockchain R&D efforts in the world. Our work bridges academia and industry, advancing decentralization, security and scalability while creating open knowledge that benefits the entire ecosystem. Whether through funding, collaboration, or partnership, contributors play a vital role in shaping innovations that are ethical, impactful and built to endure.