
Bithoven — это язык смарт-контрактов для создания мощных и безопасных инструментов на Bitcoin. LR(1)-парсер со статическим анализом для обеспечения безопасности на этапе компиляции. Статья о формальной верификации: https://arxiv.org/abs/2601.01436
Высокоуровневый императивный язык для Bitcoin-смарт-контрактов
Bithoven — это типобезопасный, удобный для разработчика язык программирования, предназначенный для компиляции в нативный Bitcoin Script. Он устраняет разрыв между сложной логикой смарт-контрактов и низкоуровневой стековой машиной Bitcoin Virtual Machine (VM).
Пишите читаемый и проверяемый код с современными управляющими конструкциями (if/else), именованными переменными и встроенными проверками безопасности — затем компилируйте его в высокооптимизированный Bitcoin Script для SegWit или Taproot.
if, else и return, вместо манипуляций со стеком в голове.bool, signature, string и для предотвращения типичных ошибок времени выполнения.numberlegacy, segwit и taproot через прагмы.older, after), криптографии (sha256, checksig) и верификации (verify).# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven
Контракты Bithoven определяются с расширением .bithoven. Ниже представлена реализация стандартного Hashed Time-Locked Contract (HTLC), демонстрирующая, как Bithoven упрощает условные пути траты.
htlc.bithoven
pragma bithoven version 0.0.1;
pragma bithoven target segwit;
/* * Stack Input Definitions
* Each line defines a valid input stack configuration for a spending path.
*/
(condition: bool, sig_alice: signature)
(condition: bool, preimage: string, sig_bob: signature)
{
// If 'condition' is true, we enter the Refund Path (Alice)
if condition {
// Enforce relative timelock of 1000 blocks
older 1000;
// If timelock is satisfied, Alice can spend with her signature
return checksig(sig_alice, "0245a6b3f8eeab8e88501a9a25391318dce9bf35e24c377ee82799543606bf5212");
} else {
// Redeem Path (Bob)
// Bob must reveal the secret preimage that hashes to the expected value
verify sha256(sha256(preimage)) == "53de742e2e323e3290234052a702458589c30d2c813bf9f866bef1b651c4e45f";
// If hash matches, Bob can spend with his signature
return checksig(sig_bob, "0345a6b3f8eeab8e88501a9a25391318dce9bf35e24c377ee82799543606bf5212");
}
}
Bithoven содержит богатую коллекцию примеров, демонстрирующих реальные Bitcoin-смарт-контракты:
| Пример | Описание | Ключевые особенности |
|---|---|---|
| HTLC | Hash Time-Locked Contract (контракт с хэш-блокировкой) | Хэш-локи, таймлоки, условные платежи |
| Atomic Swap 🆕 | Кроссчейн-обмен | Двойные SHA256 хэш-локи, доверительный обмен |
| Escrow 🆕 | Маркетплейс с мультисигом 2-из-3 | Арбитр, продавец/покупатель, возвраты с таймлоком |
| Vault 🆕 | Кошелёк с усиленной безопасностью | Отложенные во времени выводы, немедленное восстановление холодного хранилища |
| Multisig Voting 🆕 | Казначейство DAO / одобрение совета | Голосование с порогом 2-из-3, аварийное переопределение 3-из-3 |
| Prediction Market 🆕 | Децентрализованные ставки с хэш-оракулом | Криптографические схемы обязательств, проверка доказательств оракула |
| Multisig | Мультисиг 2-из-2 | Поддержка мультиподписи Taproot |
| Inheritance | Многоуровневый контроль доступа | Несколько уровней наследников, доступ на основе секрета |
| Hashlock | Простой хэш-лок | Проверка SHA256-хэша |
| Timelock | Абсолютный таймлок | CLTV (CheckLockTimeVerify) |
Все примеры: Каталог примеров
При компиляции Bithoven преобразует высокоуровневую императивную логику в эквивалентные опкоды Bitcoin Script, автоматически обрабатывая управляющие конструкции и управление стеком.
Команда:
bithoven compile htlc.bithoven
Сгенерированный Bitcoin Script (ASM):
OP_IF
<0xe803> OP_CHECKSEQUENCEVERIFY OP_DROP
<pubkey_alice> OP_CHECKSIG
OP_ELSE
OP_HASH256 OP_TOALTSTACK <hash_digest> OP_FROMALTSTACK OP_SWAP OP_EQUALVERIFY
<pubkey_bob> OP_CHECKSIG
OP_ENDIF
older <n>: Устанавливает относительный таймлок (Sequence).after <n>: Устанавливает абсолютный таймлок (LockTime).checksig(sig, pubkey): Проверяет подпись на соответствие открытому ключу.verify <expr>: Гарантирует, что выражение истинно, иначе скрипт завершается ошибкой.bool: Логические значения (true, false).signature: Подписи ECSDA или Schnorr.string: Шестнадцатеричные или ASCII строковые данные.number: Целочисленные значения.Вклад приветствуется! Пожалуйста, посетите страницу issues для пунктов дорожной карты или отправьте PR.
Этот проект лицензирован в соответствии с MIT License — подробности см. в файле LICENSE.
Если вы используете Bithoven в своих исследованиях, пожалуйста, процитируйте следующую статью:
Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts. Hyunhum Cho and Ik Rae Jeong, 2026. arXiv preprint arXiv:2601.01436. https://arxiv.org/abs/2601.01436
BibTeX:
@misc{bithoven,
title={Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts},
author={Hyunhum Cho and Ik Rae Jeong},
year={2026},
eprint={2601.01436},
archivePrefix={arXiv},
primaryClass={cs.CR},
url={https://arxiv.org/abs/2601.01436},
}
| Single Sig | Базовая проверка подписи | Простой контракт в стиле P2PKH |