FICHA · MANJARO

rocqide

Interactive theorem prover, or proof assistant (GTK-based GUI)

  • App
  • GUI
  • Launchable
official+codex · reviewed · May 29, 2026 description in en

Description

Provides a GTK-based graphical interface for Rocq proof development, helping users edit proof scripts and inspect proof state visually. It is useful for learning, teaching, and working on formal proofs with a more guided interface than a plain terminal.

The GUI improves workflow but does not replace understanding the proof assumptions. Check imported libraries, proof goals, and generated artifacts before relying on formal verification claims.

How to run

rocqide

Commands: rocqide

Permissions

Permissions not analysed for this source yet.