alt Hacker News> ... But we expect, in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have.
Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)
Replies
Mandatory Background:
1) Understanding Formal Methods by Jean-Francois Monin - This is the absolute best for getting a grip on the breadth, concepts and sample tools for Formal Mathematics/Specification/Verification. Fire-hose of information (not a step-by-step textbook) so use this as a map for everything "Formal". The S/N ratio is very high (~250 pages only!) so use AI/Textbooks to help explain concepts you find difficult to understand.
Practical:
1) Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - Uses "Alloy" language to teach Structural (i.e. Data) Modeling.
2) Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport - Uses "TLA+" language to teach Behavioural (i.e. State Machine) modeling.
The above two are for "System Modeling" i.e. everything needed to formally build complete systems.
3) Finally, You should also look at the bunch of free books on the Lean4 website which can be studied parallely for "code-level" proofs and verification.
PS: There are a few more (eg. Event-B method etc.) but you can get to those if/when you need to.
Lamport’s book and or Hillel Wayne’s are both good. State machines as a specification language has always been pretty approachable and also relatively deep. If you want to get in to proof assistants Software Foundations is great and the delta to understanding Lean from Rocq is pretty small.
https://lamport.azurewebsites.net/tla/book.html https://logicforprogrammers.com/ https://softwarefoundations.cis.upenn.edu/