# Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control


## Code in Agda
* All Agda Code
  [ScriptTester](/ScriptTester/)
  
* The file  [guidelines.agda](ScriptTester/guidelines.agda/) shows the code in the order as  it appears in the paper.

* Html version of Agda code (no Agda installation needed) In order to render it in your browser you need to download it first and then load the downloaded file html/loadAll.html into your browser. Location of files: [html](/html/loadAll.html)