CS 227 Proof Tools

Learn moves in the guided lab, assemble proofs in the checker, or write complete proofs in the compiler-style Pro workspace.

Proof Lab

Build guided proofs one justified move at a time. The lab tracks the current goal and the pretend worlds that are open.

Open the guided lab

Proof Checker

Enter axioms, a goal, and your own proof. Check each line’s formula, justification, references, and scope.

Open the checker

Proof Checker Pro

Write a complete proof as a small program. The compiler checks each command and shows the current goal and open pretend worlds.

Open the Pro checker

All three tools run entirely in your browser. New to compiler mode? Read the Proof Checker Pro guide.