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
Jasmin is a
framework for developing high-speed and high-assurance cryptographic
software. The framework is structured around the Jasmin programming
language and its compiler. The language is designed for enhancing
portability of programs and for simplifying verification tasks. The
compiler is designed to achieve predictability and efficiency of the
output code (currently limited to x64 platforms), and is formally
verified in the Coq proof assistant.
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.