Formal verification
Program = Proof is a nice book.
Notes
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) (HN)
- 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) (Web)
- 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.
- Safety and Liveness Properties (2022)
- The Hitchhiker’s Guide to Logical Verification
- State of the art for formal verification (2022)
- Why are you being constructive? (2022)
- Extracting a Verified Interpreter from Isabelle/HOL (2022)
- Solving the Dog-Bunny Puzzle with Program Verification Technology (2022)
- Silver - Intermediate verification language of the Viper project.
- Viper – Programming Methodology Group | ETH Zurich (GitHub)
- Silicon - Symbolic-execution-based verifier for the Viper intermediate verification language.
- Carbon - Verification-condition-generation-based verifier for the Viper intermediate verification language.
- ViperServer - HTTP server that manages verification requests to different tools from the Viper tool stack.
- Verifying distributed systems with Isabelle/HOL (2022) (HN)
- "Formal Modeling and Analysis of Distributed Systems" by Ankush Desai (2022)
- Keynote: Formal Methods at Microsoft - Nikolaj Bjørner (2022)
- Obtaining Statistical Properties by Simulating Specs with TLC - Jack Vanlightly and Markus A. Kuppe (2022)
- Verifying GCC optimizations using an SMT solver (2022) (HN)
- Tamarin - Security protocol verification tool that supports both falsification and unbounded verification in the symbolic model. (Web)
- OSS CAD Suite - Multi-platform nightly builds of open source digital design and verification tools.
- Let's Prove Leftpad (2022)
- ProofNet - Benchmark for undergraduate-level formal mathematics.
- Formal verification tools
- The Case for Models (2022)
- Combining Model Checking and Testing (2016) (Lobsters)
- Proofs about programs - interactive tutorial (Lobsters)
- Thoughts on user interfaces for theorem provers (2022)
- Logical Verification 2022–2023
- The Hitchhiker’s Guide to Logical Verification (2022)
- Modeling Database Tables in Alloy (2023)
- Modular Formal Verification of Rust Programs with Unsafe Blocks (2022)
- Symbolic execution engine powering the K Framework
- Refinement through Restraint: Bringing Down the Cost of Verification (2017)
- Verifiable Software Development Estimations (Lobsters)
- Quint - Specification language based on the Temporal Logic of Actions.
- Formalizing a new proof that the square root of two is irrational (2023)
- SuperNova: Proving universal machine executions without universal circuits (2022) (Code)
- Get Started with Open Source Formal Verification (2023) (HN)
- PhD Defense - Formal Verification of Just-in-Time Compilation (2023)
- Static Program Analysis (2022)
- How Kani helped find bugs in Hifitime (2023)
- What I've Learned About Formal Methods In Half a Year (2023)
- Chyp - Interactive theorem prover for string diagrams.
- Mizar proof checker
- Formal Software Design with Alloy 6
- Property-Based Testing: Climbing the Stairway to Verification (2022)
- Using z3 To Solve Logic Puzzles (2023)