A formal analysis of FLEX and FLEX2

Ramses Fernandez

Paper 2026/983

A formal analysis of FLEX and FLEX2

Ramses Fernandez, Fairgate Labs

Abstract

This paper formalizes the cryptographic core of the FLEX protocol and its enhanced variation FLEX2 . The analysis formalizes a minimal ledger abstraction, capturing Taproot, CSV timelocks, and reorg bounds, and defines ideal functionalities implemented as transaction-DAG and state machines. Main contributions include proving on-chain enforceability, CDS secrecy, soundness, leakage-bounded privacy, and universal composability realization under standard assumptions.

Note: Minor typos detected and amended

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Preprint.
Keywords: BitVM Cross-chain bridges Garbled circuits Conditional Disclosure of Secrets
Contact author(s): ramses fernandez @ fairgate io
History: 2026-05-21: revised; 2026-05-18: received; See all versions
Short URL: https://ia.cr/2026/983
License: CC BY

BibTeX

@misc{cryptoeprint:2026/983,
      author = {Ramses Fernandez},
      title = {A formal analysis of {FLEX} and {FLEX2}},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/983},
      year = {2026},
      url = {https://eprint.iacr.org/2026/983}
}