Bithoven: A Formally Verified, Imperative Smart Contract Language for Bitcoin

Bithoven stands as a general-purpose language crafted for Bitcoin Script, distinct in its approach by not being confined to specific use cases such as covenants. The primary aim behind Bithoven is to offer developers a broad spectrum of flexibility while ensuring there is no compromise on the core consensus compatibility. This ensures that developers can work within a framework that offers both freedom and adherence to essential Bitcoin protocols. The future of Bithoven includes plans for expansion and support for new features. Specifically, the integration of covenants into Bithoven is a high priority once they are activated on the mainnet. This indicates a forward-looking approach to development, where upcoming Bitcoin network features are anticipated and prepared for, thus promising continued relevance and utility of Bithoven in the evolving landscape of Bitcoin scripting.