Formal Methods Tools

At a Glance

Applications Theorem Prover
Developers Technische Universitat Munchen University of Cambridge
Inputs Isabelle
Interfaces CLI
Licenses BSD-2-Clause
Maintenance Actively Maintained

Description

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.