• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
        • Bip32
        • Bech32
        • Bip39
        • Bip44
        • Base58
        • Bip43
        • Bytes
        • Base58check
        • Cryptography
        • Bip-350
        • Bip-173
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Kestrel-books
• Projects

Bitcoin

A library for Bitcoin.

Currently this library contains a formal model of some aspects of Bitcoin. It is expected that this library will be extended with more Bitcoin-related formalizations and tools.

This library is based on the following sources:

• The Bitcoin web site, referenced as `[Site]' in the documentation of this library.
• The Bitcoin Wiki, referenced as `[Wiki]' in the documentation of this library.
• The Bitcoin Improvement Proposals (BIPs) repository, particularly the .mediawiki files. In the documentation of this library, we reference individual BIPs as `[BIPn]', where n is the number of the BIP.
• The Bitcoin White Paper, referenced as `[WP]' in the documentation of this library.
• The `Mastering Bitcoin' book, referenced as `[MB]' in the documentation of this library.

Subtopics

Bip32

Bitcoin Improvement Proposal (BIP) 32.

Bech32

A library for Bech32 encoding.

Bip39

Bitcoin Improvement Proposal (BIP) 39.

Bip44

Bitcoin Improvement Proposal (BIP) 44.

Base58

Base58 encoding and decoding.

Bip43

Bitcoin Improvement Proposal (BIP) 43.

Bytes

Bytes.

Base58check

Base58Check encoding.

Cryptography

Cryptography in Bitcoin.

Bip-350

BIP-350

Bip-173

BIP-173