A Formal analysis of Flex & Flex 2 Collaterals
Most BitVM-style bridges rely on permanent security bonds locked on-chain at all times. While effective, this model creates substantial capital inefficiencies for operators and challengers. The research presented in Ramses Fernandez’s “A Formal Analysis of FLEX and FLEX2” formalizes a different design paradigm: on-demand bonds, where collateral is only activated during disputes. This approach significantly reduces idle capital requirements while preserving the security guarantees required for optimistic dispute systems.
At the center of FLEX is a combination of Bitcoin-native primitives — Taproot, CheckSequenceVerify (CSV) timelocks, and SIGHASH_ANYONECANPAY — together with cryptographic techniques based on garbled circuits and Conditional Disclosure of Secrets (CDS). This architecture enables dispute resolution systems where only the party proven correct can unlock the appropriate secret and claim funds, while minimizing idle capital requirements.
The paper provides a rigorous formalization of the FLEX and FLEX2 protocols, defining ideal functionalities, transaction-DAG/state-machine models, and a minimal ledger abstraction tailored to Bitcoin’s execution environment.
It also proves key security properties under standard cryptographic assumptions, including:
- On-chain enforceability of Taproot-based pot scripts
- Soundness guarantees preventing “wrong-winner” outcomes
- CDS secrecy and input-binding correctness
- Leakage-bounded privacy
- UC realization of FLEX and FLEX2 in a hybrid security model
- Mutual exclusion guarantees for FLEX2 early refund mechanisms
Beyond the cryptographic analysis, the paper also explores practical considerations around dispute timing windows, reorg safety margins, and sequential composition across multiple dispute instances — all highly relevant for scalable BitVM-based bridge deployments.
FLEX2 extends the original protocol with additional interlocking mechanisms designed to prevent griefing attacks, enforce transaction ordering, and allow accelerated recovery paths when challengers become unresponsive.
This research represents an important step toward more capital-efficient, trust-minimized interoperability systems built on Bitcoin.
Read the full paper here:
