Skip to content

About this page: this page is editorial guidance written for this documentation site. It summarises and links to source material; it defines no language rules. The normative rules are in the Technical Specification.

Evidence Reports

What a verification report must record, from Program Validation and Verification and Section 55: Verification Report Format:

  • The property being evaluated.
  • The verification method used.
  • The result.
  • Any assumptions required.
  • Any limitations or unresolved conditions.

From Build and Deployment, every build must produce a verification report containing source version and hash, compiler version, dependency versions, successful checks, failed checks, unverified properties, test results, and formal verification evidence.

Normative detail: Section 55. The evidence-record schema and report format are themselves open decisions (OQ-020).