Pragmatic Equivalence and Safety Checking in Cryptol
Levent Erkok, John Matthews
Appears in PLPV '09
Cryptol is a programming language designed for specifying and
programming cryptographic algorithms. In order to meet
high-assurance requirements, Cryptol comes with a suite of
formal-methods based tools allowing users to perform various program
verification tasks. In the fully automated mode, Cryptol uses modern
off-the-shelf SAT and SMT solvers to perform verification in a
push-button manner. In the manual mode, Cryptol produces Isabelle/HOL
specifications that can be interactively verified using the
Isabelle theorem prover. In this paper, we provide an overview of
Cryptol's verification toolset, describing our experiences with
building a practical programming environment with dedicated support
for formal verification.