Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. - Fahad F. Alhabardi; Arnold Beckmann; Bogdan Lazar; Anton Setzer (TYPES, 2021)

Verification of Bitcoin's Smart Contracts in Agda using Weakest Preconditions for Access Control. - Fahad F. Alhabardi; Arnold Beckmann; Bogdan Lazar; Anton Setzer (CoRR, 2022)

A model of Solidity-style smart contracts in the theorem prover Agda. - Fahad F. Alhabardi; Anton Setzer (AIBThings, 2023)

A simulator of Solidity-style smart contracts in the theorem prover Agda. - Fahad F. Alhabardi; Anton Setzer (ICBTA, 2023)