Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts

• URL: http://arxiv.org/abs/2601.01436v1
• Date: Sun, 04 Jan 2026 08:48:34 GMT
• Title: Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts
• Authors: Hyunhum Cho, Ik Rae Jeong,
• Abstract summary: This paper introduces Bithoven, a high-level language designed to bridge the gap between expressiveness and formal safety.<n>By integrating a strict type checker and a resource liveness analyzer with a semantic control-flow analyzer, Bithoven eliminates major categories of consensus and logic defects.
• Score: 0.6187780920448871
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The rigorous security model of Bitcoin's UTXO architecture often comes at the cost of developer usability, forcing a reliance on manual stack manipulation that leads to critical financial vulnerabilities like signature malleability, unspendable states and unconstrained execution paths. Industry standards such as Miniscript provide necessary abstractions for policy verification but do not model the full imperative logic required for complex contracts, leaving gaps in state management and resource liveness. This paper introduces Bithoven, a high-level language designed to bridge the gap between expressiveness and formal safety. By integrating a strict type checker and a resource liveness analyzer with a semantic control-flow analyzer, Bithoven eliminates major categories of consensus and logic defects defined in our fault model prior to deployment. Our results indicate that this safety comes at modest cost: Bithoven compiles to Bitcoin Script with efficiency comparable to hand-optimized code, demonstrating that type-safe, developer-friendly abstractions are viable even within the strict byte-size constraints of the Bitcoin blockchain.

Related papers

• Towards Automating Blockchain Consensus Verification with IsabeLLM [1.9336815376402718]
  We present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs.<n>We demonstrate the effectiveness of IsabeLLM by using it to develop a novel model of Bitcoin's Proof of Work consensus protocol and verify its correctness.
  arXiv  Detail & Related papers  (2026-01-12T15:35:08Z)
• SEDULity: A Proof-of-Learning Framework for Distributed and Secure Blockchains with Efficient Useful Work [41.41842611951311]
  We name the framework SEDULity, which stands for a Secure, Efficient, Distributed, and Useful Learning-based blockchain system.<n>We show that our framework is distributed, secure, and efficiently trains ML models.<n>We further demonstrate that the proposed PoL framework can be extended to other types of useful work and design an incentive mechanism to incentivize task verification.
  arXiv  Detail & Related papers  (2025-12-15T18:55:20Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• BlockScan: Detecting Anomalies in Blockchain Transactions [16.73896087813861]
  BlockScan is a customized Transformer for anomaly detection in blockchain transactions.<n>This work sets a new benchmark for applying Transformer-based approaches in blockchain data analysis.
  arXiv  Detail & Related papers  (2024-10-05T05:11:34Z)
• FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols [7.413607595641641]
  We introduce Foray, a highly effective attack synthesis framework against deep logical bugs in DeFi protocols. Based on our DSL, we first compile a given DeFi protocol into a token flow graph, our graphical representation of DeFi protocols. Then, we design an efficient sketch generation method to synthesize attack sketches for a certain attack goal.
  arXiv  Detail & Related papers  (2024-07-08T19:35:48Z)
• Secure compilation of rich smart contracts on poor UTXO blockchains [0.8192907805418581]
  We present ILLUM, an Intermediate-Level Language for the UTXO Model. We define a compiler from ILLUM to a bare-bone UTXO blockchain with loop-free scripts. We exploit covenants, a mechanism for preserving scripts along chains of transactions.
  arXiv  Detail & Related papers  (2023-05-16T15:40:18Z)
• Blockchain Large Language Models [65.7726590159576]
  This paper presents a dynamic, real-time approach to detecting anomalous blockchain transactions. The proposed tool, BlockGPT, generates tracing representations of blockchain activity and trains from scratch a large language model to act as a real-time Intrusion Detection System.
  arXiv  Detail & Related papers  (2023-04-25T11:56:18Z)
• A formal model for ledger management systems based on contracts and temporal logic [0.0]
  In second-generation blockchains such as the ledger is coupled with smart contracts. The current implementation of smart contracts as arbitrary programming constructs has made them susceptible to dangerous bugs. We propose here to recompose the split and recover the reliability of databases by formalizing a notion of contract modelled as a finite-state automaton.
  arXiv  Detail & Related papers  (2021-09-30T15:34:28Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  Existing machine learning-based vulnerability detection methods are limited and only inspect whether the smart contract is vulnerable. We propose ESCORT, the first Deep Neural Network (DNN)-based vulnerability detection framework for smart contracts. We show that ESCORT achieves an average F1-score of 95% on six vulnerability types and the detection time is 0.02 seconds per contract.
  arXiv  Detail & Related papers  (2021-03-23T15:04:44Z)
• Robust Blockchained Federated Learning with Model Validation and Proof-of-Stake Inspired Consensus [43.12040317316018]
  Federated learning (FL) is a promising distributed learning solution that only exchanges model parameters without revealing raw data. We propose a blockchain-based decentralized FL framework, termed VBFL, by exploiting two mechanisms in a blockchained architecture. With 15% of malicious devices, VBFL achieves 87% accuracy, which is 7.4x higher than Vanilla FL.
  arXiv  Detail & Related papers  (2021-01-09T06:30:38Z)
• Quantum Multi-Solution Bernoulli Search with Applications to Bitcoin's Post-Quantum Security [67.06003361150228]
  A proof of work (PoW) is an important cryptographic construct enabling a party to convince others that they invested some effort in solving a computational task. In this work, we examine the hardness of finding such chain of PoWs against quantum strategies. We prove that the chain of PoWs problem reduces to a problem we call multi-solution Bernoulli search, for which we establish its quantum query complexity.
  arXiv  Detail & Related papers  (2020-12-30T18:03:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.