Formal verification

Program = Proof is a nice book.

Notes

• I like to start with a full english description, and then write things as FOL predicates. The act of translating it into math, even "sloppy" math, is a great first past for seeing issues more clearly. If it passes that, then I move on to FM.

Links

• What, Why, and How of Formal Methods (2019)
• Why don't people use formal methods? (2019) (HN)
• F* - Verification system for effectful programs.
• HOL Light - Computer program to help users prove interesting mathematical theorems completely formally in higher order logic.
• Verified Software Toolchain - Includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language.
• MIT Programming Languages & Verification Group
• Encyclopedia of Proof Systems
• A Domain-Specific Language for Verifying Software Requirement Constraints
• Provably Correct Peephole Optimizations with Alive (2019)
• SwiftCSP - Constraint satisfaction problem solver written in pure Swift.
• Proof Assistants At the Hardware-Software Interface (2020)
• The business case for formal methods (2020) (Lobsters) (HN)
• Logipedia - Project that aims to share formal proofs between several systems.
• Alloy - Language for describing structures and a tool for exploring them. (Docs) (Article) (Lobsters) (Tweet) (Being Formal Yet Lightweight)
• Alloy 6 First Impressions (2021)
• Software Abstractions book
• Safe and Efficient, Now
• Experiences moving from tests to strong typing? (2020)
• Margin in Software Systems (2010)
• SyGuS competition - Allow solvers for syntax-guided synthesis problems to compete on a large collection of benchmarks.
• Verification Competitions (2020)
• K Framework – An Overview (2018)
• Learning to Prove Theorems via Interacting with Proof Assistants (2019)
• How do I rigorously translate a spec to implementation, and how do I keep them in sync? (2020)
• Engineering a Safer World notes
• Separation Logic (2019)
• List of companies that use formal verification methods in software engineering
• Formal Specification and Taming Other People's Tech - Marianne Bellotti (2019)
• Verified Programming with Project Everest (2020)
• Proving Algebraic Datatypes are “Algebraic” (2020)
• SPLV – Scottish Programming Languages and Verification Summer School
• backspace.ai - Fun resource to start playing with formal programming languages.
• Formulog: ML + Datalog + SMT (2020)
• An introduction to Formal Verification for Software Systems (2020)
• Proof Engineering - Specifying, building, verifying, and maintaining software systems using proof assistants such as Coq, Isabelle/HOL, and HOL4.
• Software Engineering and Formal Methods 2020
• The Assembly Language of Satisfiability (2020)
• Continuous compliance with lightweight verification tools (2020)
• Runtime Verification - Startup company aimed at using runtime verification-based techniques to improve the safety, reliability, and correctness of software systems.
• Crucible - Language-agnostic library for performing forward symbolic execution of imperative programs. It provides a collection of data-structures and APIs for expressing programs as control-flow graphs. (Web) (Intro)
• snarky - OCaml DSL for verifiable computation.
• Proofs Should Repair Themselves (2020) (Lobsters)
• Use polling for resiliency (2020) (Lobsters)
• The 2020 Expert Survey on Formal Methods
• Formal Methods for the Informal Engineer (2020) (Code)
• Finding Software Bugs Using Symbolic Execution (2020)
• MiniZinc - High-level constraint modelling language that allows you to easily express and solve discrete optimization problems. (Code) (Solving River Crossing Puzzles With MiniZinc)
• FMathL - Formal Mathematical Language.
• Dafny - Verification-aware programming language. (Docs)
• Formal Methods Research Group - University of Glasgow
• Formal Methods: An Appetizer (2019)
• Software Verification and Analysis Using Z3 (2021)
• Program = Proof - Gives a first introduction to the Curry-Howard correspondence between programs and proofs. (Lobsters)
• Concrete Semantics - Introduces semantics of programming languages through the medium of a proof assistant.
• Curry-Howard is a scam (2021) (Lobsters)
• Computing with metavalues (2021)
• CLP - Open-source linear programming solver.
• Metamath Zero - Language for writing specifications and proofs. Its emphasis is on balancing simplicity of verification and human readability of the specification.
• KreMLin - Tool for extracting low-level F* programs to readable C code.
• Formal Methods of Software Design Course by Eric Hehner (HN)
• The Little Prover (Code)
• IncA - Incremental Program Analysis Framework.
• Combining static model checking with dynamic enforcement using the Statecall Policy Language (2015)
• Proofcraft - Partner with experts to verify your software. Learn formal verification from the experts.
• Can Formal Methods Succeed where UML Failed? (2021)
• Verification = TCB/PB Reduction (2021) (Lobsters)
• Copilot - Stream-based runtime-verification framework for generating hard real-time C code.
• Software Foundations Lab
• Where are we going from here? Software engineering needs formal methods (2021) (HN)
• Extending Event-B with Discrete, Timing Properties (2012)
• Esther - Automated theorem proof assistant based on Homotopy Type Theory.
• Is the formal methods winter about to end? (2021)
• Pantagruel - Extremely Lightweight Specification Language. (HN)
• There Was No Formal Methods Winter (2021)
• REMS (Rigorous Engineering of Mainstream Systems) (GitHub)
• The Curry-Howard Correspondence (2021)
• SAWScript - Scripting language that forms the primary user interface to the Software Analysis Workbench (SAW).
• You Already Know Formal Methods (2021) (HN)
• Verification For Dummies: SMT and Induction Book
• Formal verification/analysis tools tutorials
• hoice - ICE-based predicate synthesizer for Horn clauses.
• Higher-Order Program Verification
• SMACK - Software Verifier and Verification Toolchain. (Web)
• A Tool for Producing Verified, Explainable Proofs Thesis (2021) (Code)
• Cogent: uniqueness types and certifying compilation (2021) (Tweet)
• Anatomy of a STARK - Tutorial explaining the mechanics of the STARK proof system. (HN) (Code)
• Kind - Minimal, efficient and practical programming language that aims to rethink functional programming from the scratch, and make it right. (Code) (Theorem Proving)
• Beyond inductive datatypes: exploring Self types
• Misspecification: The Blind Spot of Formal Verification (2021) (Lobsters)
• Verification-Driven Development Guide
• Electrum Analyzer - Model checker for relational first-order temporal specifications. (Tutorial)
• Simple proof checker in OCaml
• Provably-correct versions of Leftpad
• Structured derivations: a unified proof style for teaching mathematics (Tweet)
• Gospel - Tool-agnostic formal specification language for OCaml. (Docs)
• Alloy 6: it's about Time (2021) (Lobsters)
• Refinement: Formalizing the Simplicity Underneath Complex Programs (2021)
• Automated theorem prover for first-order logic
• ProvingGround - Tools for Automated Mathematics.
• LARA – Lab for Automated Reasoning and Analysis
• Formal verification of IA-64 division algorithms
• rzk - Prototype interactive proof assistant based on a type theory for synthetic ∞-categories.
• A Manifesto for Applicable Formal Methods (2021)
• Autosubst OCaml - OCaml reimplementation of the Autosubst 2 code generator.
• Using lightweight formal methods to validate a key-value storage node in Amazon S3 (2021)
• Less is more: multiparty session types revisited (2019) (Lobsters)
• Machine Readable Specifications at Scale (2022) (HN)
• CMU Program Analysis Course (2022) (Code)
• MIT Formal Reasoning About Programs (2022) (Code)
• Formal Verification of a Distributed Dynamic Reconfiguration Protocol (2021) (Code)
• Kimchi: The latest update to Mina’s proof system (2022) (HN)
• Cubicle - Tool that combines model checking algorithms and automatic SMT theorem provers with a powerful invariants inference mechanism. (Code)
• A gentle introduction to automated reasoning (2021)
• A Specification of a Note-Taking Program (2022) (Lobsters)
• A Survey on Automated Fact-Checking (2021) (Code)
• Pantagruel - Program specification language with a formal syntax and ad-hoc semantics. (Lobsters)
• VerifAI - Software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components.
• Formal Methods for DeFi Developers
• Yatima - Verifiable computing language.
• VeriFast - Research prototype tool for modular formal verification of C and Java programs.
• Introduction to Pragmatic Formal Modeling (Code)
• Using the Kani Rust Verifier on a Firecracker Example (2022)
• Q*Cert - Compilation and Verification of Data-Centric Languages.
• MLIR-TV - Translation validation framework for MLIR.