QED
QED (Quite Easy Deduction) is a theorem prover for higher-order logic written in MoonBit. It follows the LCF approach: a small trusted kernel implements the primitive inference rules of HOL and is the only code that can create theorems, and everything else, from the parser to the command-line tool, builds on it without being trusted. Proofs are written as short theorem scripts with goal-directed steps; a script either yields a kernel theorem, fails with a structured diagnostic, or reports an unfinished proof. A formal specification defines the kernel, and a Lean 4 pack in formal_verification/ checks the specification’s conformance claims.
The shipped proof language covers propositional logic with equality, theorem-header binders and goal-level forall; the user manual has the exact support matrix.
Formal specification
The formal specification is the only normative source for the kernel.
Packages
The packages are layered: each depends only on packages to its left, kernel → logic/elab → parser → tactics → prover → cmd, and only kernel is trusted.
| Package | Role | Pages |
|---|---|---|
kernel | Trusted kernel: types, terms, the abstract theorem type, primitive rules, scoped signature, extension gates | API · design · tutorial |
logic | Propositional connectives as definitions, derived rules, replay helpers, theorem catalog | API · design · tutorial |
elab | Name resolution with frozen constant identities, core typing, lowering to kernel terms | API · design · tutorial |
parser | Text frontend: normalisation, terms, goals, theorem scripts, source positions | API · design · tutorial |
tactics | Backward proof states and steps, replayed forward to kernel theorems | API · design · tutorial |
prover | Theorem-script driver with structured results, and the regression corpus | API · design · tutorial |
cmd | The command-line tool qed-cmd (executable package) | API · design · tutorial |
research_rewrite | Research-only rewriting prototype, not shipped | API · design · tutorial |
Blackbox test files (*_test.mbt) and the alias files alias.mbt and alias_test.mbt belong to their packages; code governance defines their rules. The theorem files in examples/ and prelude/ are inputs for the command-line tool, not packages.
Where to start
New to proof assistants. Read “For readers new to HOL” and the quick start in the user manual, then run the examples with the cmd tutorial. The syntax guide answers “how do I write this step”.
Using QED from MoonBit. Start with the prover tutorial to run scripts and read results. Go down to the tactics tutorial to drive proofs step by step, and to the logic and kernel tutorials to build theorems forwards.
Checking why it is sound. Read the kernel design, which derives the rules and explains why soundness reduces to the kernel, then the logic and tactics designs, which show that the upper layers add no authority. The formal specification above is normative.
Contributing. Read code governance and documentation governance first, then specification conformance for the code/test mapping and the rules for examples. The workspace audit lists open risks; the specification changelog records revisions of the specification.
Guides
- User manual: the user guide and implementation contract, with the support matrix and the stable examples.
- Syntax guide: the theorem-script syntax.
- Specification conformance: how code and tests align with the specification, and what contributors must do.
- Documentation governance and Code governance: repository rules for documents, package layering and alias entry points.
- Formal specification changelog: revisions of the specification.
- Workspace audit (2026-04-18): a point-in-time record of risks and gaps.
Install and build
QED requires the MoonBit toolchain with moonc 0.10 or later, and depends on moonbitlang/x for file access in the command-line tool. To use the library from another module:
moon add Luna-Flow/QED@0.1.0To work in the repository:
moon check --target all
moon test
moon run src/cmd examples/truth_file.qedThe Lean formalisation builds separately with lake build in formal_verification/.