Terminology
The formal theory separates several objects that are often collapsed in informal assurance discussions.
A world represents a possible state relevant to evaluation. A world space specifies which worlds are admissible for an analysis.
A claim is a predicate over worlds.
Evidence is information that may be available to an evaluator.
Evaluator conditions represent the evaluator's knowledge, access, trust, and cooperation conditions.
A budget represents resource constraints affecting what evidence can practically be obtained.
An assurance context combines the claim and evaluation conditions used to reason about a system.
An evidentiary capability represents a distinction or evaluative operation enabled by claim-material evidence.
These descriptions are explanatory only. The Lean declarations are authoritative.