V. Coq proof assistant

1. Presentation
   CoqIDE makes it possible to:
   1. Define functional programs P,
   2. Specify properties S of the program, and
   3. Prove these properties by using rewriting rules - ie. conformance of the program to the specification:

S |= P

source

On Linux (eg. Debian or Ubuntu) systems, you can easily install the tool with:

apt update && apt install -y coqide

1 - 7