Sequent is a Fitch-style first-order logic proof language and web app for checking, formatting, and rendering proofs with clickable diagnostics.