Specifying Smart Contracts with Hax and ConCert

Explore the advancements in high-assurance smart contracts through this 16-minute conference talk from ACM SIGPLAN's CoqPL'24. Delve into the Hax toolchain and its integration with ConCert, presented by Lasse Letager Hansen and Bas Spitters. Learn how software engineers can embed smart contracts to generate clean Rust code, incorporate security properties and guarantees directly into the code using Hax, and subsequently translate these specifications into ConCert for verification. Gain insights into the ongoing efforts to extend high-assurance practices from cryptographic software to smart contracts, enhancing their reliability and security.

[CoqPL'24] Specifying Smart Contract with Hax and ConCert