I'm looking to learn more about formally specifying the requirements for a piece of software, modelling and simulating the design, and verifying its correctness with a proof assistant or model-checker. Thanks!