Formal verification is really hard because you have to use mathematical proof to show that a piece of software does what it should on all inputs and paths. You

Formal verification is really hard because you have to use mathematical proof to show that a piece of software does what it should on all inputs and paths. You have to formalize the software, the desired goals, and prove a connection. Typically, you have to do this for software written in languages that aren't designed for verification. That makes it even harder. This led me to recommend people start with so-called lightweight, formal methods that require less upfront learning with more automation. You'll see the value of formal methods, have more fun, and maybe use it on realistic problems. The best one to start with is Design-by-Contract invented by Meyer in the 1980's based on principles from 1960's. Contracts are simply precise, declarative descriptions of a module expects from callers, does during execution, and returns to the caller. Here's an overview even a project manager can find useful: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... A number of us independently arrived at a specific use for contracts that's high ROI. You use contracts to specify intent, then automatically generate tests from them (replaces unit testing), and finally they can become runtime checks for automated testing (esp fuzzing). Contract-based tests or fuzzing with contract-based checks cause each failure to take you right to the source of the problem. Note that the test generation part has many names to Google: specification- or spec-based, model-based, and recently property-based testing. Hillel Wayne has great posts on contracts and test generation: https://hillelwayne.com/post/contracts/ https://hillelwayne.com/post/contracts/ https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/ I recommend reading his whole blog. Anyway, the next tool is Alloy which is super-simple but with better tooling than most academic works. Hillel has examples on his blog. Davidk01 on Lobste.rs has been using it for a lot of things. He said, given its relational, he just uses it like he uses SQL: https://lobste.rs/s/ghhcus/test_generation_from_bounded_algebraic#c_ucipzt https://lobste.rs/s/ghhcus/test_generation_from_bounded_alge... Finally, one that will help you with protocols and concurrency is TLA+. Hillel has learntla.com up to teach you for free on top of blog examples. After a lot more time with it, he got to publish a book through Apress. I recommend it: https://www.betterworldbooks.com/product/detail/Practical-TLA---Planning-Driven-Development-9781484238288 https://www.betterworldbooks.com/product/detail/Practical-TL... If you want a taste of proof, the SPARK Ada language was designed to make it easier. It's used in industry. Basically uses contract-like specs and supporting functions to feed "verification conditions" into automated solvers. You only have to prove what they can't but can always use runtime checks on those. There's a nice book teaching you how to use it plus Altran/Praxis' Correct-by-Construction method for low-defect software. https://www.betterworldbooks.com/product/detail/Building-High-Integrity-Applications-with-SPARK-9781107656840 https://www.betterworldbooks.com/product/detail/Building-Hig... There's also Cleanroom: a 1980's method that combines semi-formal specs, simple use of language, hierarchical composition, and usage-based testing to cost-effectively get high quality software. Stavely has best intro to it: http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html https://www.betterworldbooks.com/product/detail/Toward-Zero-Defect-Programming-9780201385953 https://www.betterworldbooks.com/product/detail/Toward-Zero-... Note: Linking to Better World Books since they're a public-benefit type of company (see History). Amazon ain't. ;)