Formal Methods?

Very broadly, there are two domains in FM: formal specification is the study of how we write precise, unambiguous specifications, and formal verification is the study of how we prove things are correct.

Hillel Wayne in WDPUFM

In this session we ran through some examples in Coq, TLA+ and Alloy and interesting questions arose about how you can connect your verified model to your code

• Thinking for Programmers Talk by L. Lamport on why formal methods/specification (of any kind) can help you write better code
• Coq The Coq proof assistant (you should also install CoqIDE)
• RustBelt Formal proof of the soundness of the type system of Rust
• Recommendations for secure applications development with Rust The National Cybersecurity Agency of France Replacing C/C++ with Rust for safety
• Slides for TLA+/Pluscal (there are additional TLA+ links in the PDF therein) Slides (Ruben) showed with a bit of TLA+ motivation
• Why don’t people use formal methods? (Post by Hillel Wayne) A vision of the formal methods landscape, what lies where and what you can do with each tool
• Solving Knights and Knaves with Alloy (Post by Hillel Wayne) A set of easy but non-trivial examples in Alloy to show its deductive abilities
• The Alloy Analyzer You need this to run Alloy. The “Alloy Book” (Software Abstractions by Daniel Jackson linked from there) is a very accessible read
• Java goes TLA+ Formally verifying Java code, completely
• Specifying and Verifying Concurrent C Programs with TLA+ Likewise for C
• PGo: A Pluscal to Go transpiler Converting Pluscal procedure code into Go code