Tutorial

This section of the manual contains a two-part hands-on introduction to ProofFrog. Work through the parts in order:

1. Part 1: Hello Frog: Run an existing proof, break it on purpose, fix it. No proof-writing just yet.
2. Part 2: OTP has one-time secrecy: Write your first complete four-file proof from scratch, showing the security of the one-time pad.

After finishing the tutorial, continue with the Worked Examples for fully-explained walkthroughs of larger proofs.