Formal Methods logopeterindia.net
Knowledge Hub

Formal Methods Resources

Mathematically rigorous ways to specify and verify software and hardware — tools, verified systems and where to learn.

26 topics•5 categories•Updated October 2026

Proof Assistants & Provers

4 entries

Check proofs mechanically.

01LeanProof assistant and programming language, widely used in formalized mathematics. 02Rocq Prover (formerly Coq)Interactive theorem prover based on type theory. 03IsabelleGeneric proof assistant. 04Z3 Theorem ProverSMT solver from Microsoft Research.

Specification & Model Checking

4 entries

Describe and check system designs.

05TLA+Specification language for concurrent and distributed systems, by Leslie Lamport. 06AlloyLightweight modelling language and analyzer. 07SPINModel checker for verifying concurrent software. 08NuSMVSymbolic model checker.

Program Verification & Verified Systems

5 entries

Prove code correct.

09DafnyVerification-aware programming language. 10Frama-CAnalysis framework for C code. 11seL4Operating system microkernel with a machine-checked proof of correctness. 12CompCertC compiler verified in Coq. 13How Amazon Web Services Uses Formal MethodsCommunications of the ACM article on industrial use.

Learning & Community

7 entries

Books, organizations and research groups.

14Software FoundationsFree online textbook series on logic, programming languages and verification. 15Formal Methods Europe (FME)Association promoting formal methods in industry. 16Formal Methods and Dependable Systems (SRI International)Research programme. 17Formal Methods (MathWorks)Overview from MathWorks, with its own product focus. 18Formal Methods WikiCommunity wiki entry. 19ISTI-CNR Research LaboratoriesItalian research institute including formal methods groups. 20Formal Aspects of Computing (Springer)Journal on formal methods.

Related Pages

6 entries

Neighbouring pages on this site.

21Number Theory for AIIncludes AI for formal proof in Lean. 22Theoretical Computer ScienceTheoretical computer science hub. 23Complexity TheoryComputational complexity resources. 24Software TestingSoftware testing resources. 25Software EngineeringSoftware engineering hub. 26MathematicsMathematics hub.

Frequently Asked Questions

What are formal methods?

They are mathematically based techniques for specifying and verifying software and hardware, for example proving that a program meets its specification or exhaustively checking a design model.

What is the difference between a model checker and a proof assistant?

A model checker explores the states of a model automatically and reports counterexamples. A proof assistant checks proofs that a person, and increasingly an AI, constructs step by step, and can handle infinite systems.

Are formal methods used in industry?

Yes. Examples include seL4 and CompCert, and Amazon Web Services has described using TLA+ and other formal methods for cloud services.

How current is this page?

Links were checked in October 2026. Publisher and journal sites that block automated checks are kept and may need a manual click. This page lists resources rather than teaching the subject.