This project implements formal verification of Universal Composability (UC) protocols using the Quint specification language. It provides a framework for modeling UC ideal functionalities and their properties.

For this project we used Quint 0.29.1 and Apalache 0.51.1

Quint provides different modes of checking the specification. We briefly explain some of them. For more info, go to https://quint-lang.org/

In simulation mode the Quint will produce random traces and check the invariant after each "step".

quint run <spec_file> --invariant=<property> [--max-steps=n] [--max-samples=m] [--backend rust]

For example, to use simulator on all the specified properties of hash functions you can run the following code:

quint run specs/f_hash/f_hash_properties.qnt --invariant=AllProps --max-steps=500 --max-samples=10000 --backend rust

We can instruct Quint to compile its specification to TLA+ and use TLC to check the property. In this mode TLC will try to exhaustively cover the entire model to generate a counterexample.

./check_with_tlc.sh <spec_file> [--invariant <property>] [--temporal <properties>]

For example, to check with TLC all specified properties of F-PKI you can run the following code:

./check_with_tlc.sh specs/f_pki/f_pki_properties.qnt --invariant AllProps 

However, you might want to reduce the model size in common.qnt.

In this mode the Quint spec will be compiled and checked with the Apalache SMT solver.

quint verify <spec_file> [--invariant=<property>] 

For example, to verify all specified properties of Global clock with Apalache SMT solver you can run the following code:

quint verify specs/g_clock/g_clock_properties.qnt --invariant AllProps 

Model size can be set in common.qnt.

• F-iNIZK - non-interactive ZK proofs for (i - interactive) relations
• F-ATMS - Advanced threshold multi-signature scheme
• F-Hash - Hash functionality with collision resistance
• F-PKI - Public Key Infrastructure (registration, retrieval, verification)
• F-Diffuse - Message diffuse protocol
• F-Sig - digital signature primitive
• F-AC - authenticated channel
• F-CRS - common reference string

• G-Clock - Global clock for time synchronization
• G-Ledger - Global ledger with committee selection, APL, reads, and submits

• P-Bridge - Cross-chain bridge protocol built from the above functionalities

• Choreographic modeling: Explicit message passing between processes (parties, simulator, environment)
• Local context transitions: Each process defines reaction rules based on incoming messages
• Custom effects: Message exclusion and event logging for protocol control flow
• Property checking: Invariant verification via Apalache, TLC, and simulation