formal.org

Discrete Mathematics for Formal VerificationA 10-module course connecting discrete mathematics to formal verification. Learn propositional logic, set theory, temporal logic, and SAT solving through hands-on SVA exercises.Modules (10)

Module 1 — Propositional Logic and Boolean Algebra — 6 katas

Module 2 — Boolean Equivalence and Canonical Forms — 3 katas

Module 3 — Sets, One-Hot Encoding and Reachability — 4 katas

Module 4 — Relations — 4 katas

Module 5 — Predicate Logic & Quantifiers — 3 katas

Module 6 — Proof Techniques — 3 katas

Module 7 — Induction & Strengthening — 6 katas

Module 8 — State Machines and State Graphs — 6 katas

Module 9 — Temporal Logic — 4 katas

Module 10 — Engines and Scale Survey — 6 katas

Every kata runs SymbiYosys in the browser: write the properties, run the proof, read the counterexample.