Formal Methods
- Reading Tamarin Prover Output: A Visual Tutorial
- Formalizing Program Analysis in Lean 4
-
Coq Cheatsheet: Tools and Tactics for Goal Solving
Interactive reference
A quick, clickable reference to common Coq tactics. Pick a group below, then expand any card for a worked example and explanation. Tactics run from everyday building blocks to heavier proof automation.