Cover Image

Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Cho, Hyunhum, Jeong, Ik Rae
Format:	Preprint
Published:	2026
Subjects:	Cryptography and Security Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
by: Ball, Thomas, et al.
Published: (2024)

Constructing Trustworthy Smart Contracts
by: Chait-Roth, Devora, et al.
Published: (2024)

Smart Contract Languages: a comparative analysis
by: Bartoletti, Massimo, et al.
Published: (2024)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
by: Huyghebaert, Sander, et al.
Published: (2023)

Formalizing Stack Safety as a Security Property
by: Anderson, Sean Noble, et al.
Published: (2021)

Program Analysis for High-Value Smart Contract Vulnerabilities: Techniques and Insights
by: Smaragdakis, Yannis, et al.
Published: (2025)

A Language for Smart Contracts with Secure Control Flow (Technical Report)
by: Yao, Siqiu, et al.
Published: (2024)

SmartInv: Multimodal Learning for Smart Contract Invariant Inference
by: Wang, Sally Junsong, et al.
Published: (2024)

Demystifying Invariant Effectiveness for Securing Smart Contracts
by: Chen, Zhiyang, et al.
Published: (2024)

Gradual Verification for Smart Contracts
by: Sun, Haojia, et al.
Published: (2023)

Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts
by: Kong, Ziqiao, et al.
Published: (2025)

OpenTracer: A Dynamic Transaction Trace Analyzer for Smart Contract Invariant Generation and Beyond
by: Chen, Zhiyang, et al.
Published: (2024)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
by: Thibault, Jérémy, et al.
Published: (2024)

Automated Formal Verification of a Software Fault Isolation System
by: Sotoudeh, Matthew, et al.
Published: (2025)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
by: Baumann, Jonathan, et al.
Published: (2026)

Hornet Node and the Hornet DSL: A Minimal, Executable Specification for Bitcoin Consensus
by: Sharp, Toby
Published: (2025)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
by: Reitz, Antonin, et al.
Published: (2024)

Formal Modelling and Security Analysis of Bitcoin's Payment Protocol
by: Modesti, Paolo, et al.
Published: (2021)

Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
by: Amorim, Arthur, et al.
Published: (2025)

Friend or Foe Inside? Exploring In-Process Isolation to Maintain Memory Safety for Unsafe Rust
by: Gülmez, Merve, et al.
Published: (2023)

Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics
by: Chen, Haobin Hiroki, et al.
Published: (2025)

BitMLx: Secure Cross-chain Smart Contracts For Bitcoin-style Cryptocurrencies
by: Badaloni, Federico, et al.
Published: (2025)

Blockly2Hooks: Smart Contracts for Everyone with the XRP Ledger and Google Blockly
by: Trestioreanu, Lucian, et al.
Published: (2025)

A Deductive System for Contract Satisfaction Proofs
by: Correnson, Arthur, et al.
Published: (2026)

Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
by: Tempel, Sören, et al.
Published: (2024)

How To Save Fees in Bitcoin Smart Contracts: a Simple Optimistic Off-chain Protocol
by: Maddaloni, Dario, et al.
Published: (2024)

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

Protocols to Code: Formal Verification of a Next-Generation Internet Router
by: Pereira, João C., et al.
Published: (2024)

Bitcoin Smart Accounts: Trust-Minimized Native Bitcoin DeFi Infrastructure
by: Lalor, Cian, et al.
Published: (2026)

Adding Compilation Metadata To Binaries To Make Disassembly Decidable
by: Engel, Daniel, et al.
Published: (2026)

Compositional security definitions for higher-order where declassification
by: Menz, Jan, et al.
Published: (2026)

Neuroforger: certified violation witnesses for smart contracts verification via LLMs
by: Bartoletti, Massimo, et al.
Published: (2026)

SplittingSecrets: A Compiler-Based Defense for Preventing Data Memory-Dependent Prefetcher Side-Channels
by: Sharma, Reshabh K, et al.
Published: (2026)

Lightweight Yet Secure: Secure Scripting Language Generation via Lightweight LLMs
by: Zhang, Keyang, et al.
Published: (2026)

A Bayesian Approach to Membership Inference for Statistical Release
by: Oakley, Lisa, et al.
Published: (2026)

Misquoted No More: Securely Extracting F* Programs with IO
by: Andrici, Cezar-Constantin, et al.
Published: (2026)

Filament: Denning-Style Information Flow Control for Rust
by: Ching, Jeffrey C., et al.
Published: (2026)

SDLLMFuzz: Dynamic-static LLM-assisted greybox fuzzing for structured input programs
by: Zou, Yihao, et al.
Published: (2026)

Deterministic Fully-Static Whole-Binary Translation without Heuristics
by: Chen, Hongyu, et al.
Published: (2026)

PermRust: A Token-based Permission System for Rust
by: Gehring, Lukas, et al.
Published: (2025)