DY*: Symbolic protocol verification embedded in F* for executable code
======================================================================

DY* verifies protocol implementations written in F* against symbolic security properties, so the analysed model is the executable code. It has been applied to Signal and ACME and is the successor to ProScript.

Maintainer: Inria, CISPA, University of Stuttgart
Website: https://github.com/REPROSEC/dolev-yao-star
Category: Symbolic protocol analysis
Targets: Protocol implementations in F* (Signal, ACME)
Approach: Dolev-Yao reasoning inside the F* proof assistant, over executable protocol code
Access: Open source
Status: Research, active
Strengths: No model-code gap. | Composable with HACL* verified primitives.
Limits: F* implementation required. | Research maturity. | Manual proof effort.
Firms using it: none listed
Sources: https://github.com/REPROSEC/dolev-yao-star

Source page: https://sorryfree.com/frameworks/dystar/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13