EasyCrypt is a toolset
for reasoning about relational properties of probabilistic
computations with adversarial code. Its main application is the
construction and verification of game-based cryptographic
Coq Modulo Theory is an extension of the Coq proof assistant
embedding, in its computational mechanism, validity entailment for
user-defined first-order equational theories.