Formal verification
Formal verification is the use of mathematical specifications, models, and mechanically checkable reasoning to establish that a system satisfies specified properties.
Real-World Cryptography
Formal verification is the use of mathematically based languages, models, and procedures to analyze whether a system satisfies specified properties.
- How it is used
- Uses computer-assisted analysis to find subtle attacks in cryptographic protocols, especially when trusted constructions do not address the problem.
- How deep it goes
- Explains protocol translation, property expression, and false proof goals, but does not descend into formal-language syntax or proof internals.
- Examples
- Uses Tamarin to model protocols and find attacks, and mentions Verifpal as an easier tool with a soundness tradeoff.
- What you can do after
- Diagnose/debug with Tamarin by modeling a cryptographic protocol and checking stated properties for attacks.
Read how Real-World Cryptography explains formal verification →
Authorization in Action
Formal verification is the use of mathematically defined models and proofs to establish that software satisfies specified properties.
- How it is used
- Strengthens policy review by checking safety properties and whether analyzed permissions match runtime behavior.
- How deep it goes
- Explains logical encodings, SMT checking, Lean proofs, executable models, and testing, without detailing individual proof constructions.
- Examples
- Checks invoice access, unmanaged-device deployment access, and permission changes caused by policy refactoring.
- What you can do after
- Evaluate policy properties and refactorings with analyzers whose translations have mathematically proven correctness.
Read how Authorization in Action explains formal verification →
These guides are generated from the text of Manning books by Manning's knowledge graph and link to the sections they draw on. The full books are available on liveBook and at manning.com.