The next release of forall x: Calgary will include chapters on modal logic (natural deduction proof system and Kripke semantics). They are based on a Modal Logic Primer by Rob Trueman (University of York), which he was generous enough to share. I’ve changed the proof system to use Fitch’s modal rules. It covers the basics of K, T, S4, and S5. Below is a preview. If you have suggestions, please file an issue on GitHub or send a pull request (against the modal-logic branch).