Proof · Engineering practice
Software verification report: example and template
A software verification report records which requirements were checked, the software revision and environment, observed results, and unresolved gaps. It reports what happened against the verification plan; the acceptance decision remains a separate, authorized judgment.
A reusable verification-report template
Use this plain-text template in your existing documents or issue tracker. No signup needed.
Scope and purpose: Candidate code revision: Requirement IDs and revisions: Verification plan and revision: Environment, dependencies and configuration: For each check: Claim and acceptance condition: Test, analysis or review identifier: Command or procedure and producing tool: Execution time and revision: Expected observation: Actual observation: Result: not run / pass / fail / inconclusive Output or artifact location: Freshness basis and known limitations: Uncovered requirements and unexecuted cases: Failures, stale results and unresolved findings: Exceptions, authority and expiry: Acceptance decision, responsible authority and date: Reverification required after:
Keep one result record per meaningful observation. If a check has not run, leave the actual observation empty and mark it not run. Do not fill unknowns with a generated summary that sounds conclusive.
A report for one worker-pool change
This illustrative report concerns a helper that must clamp requested workers to the interval 1 through 20. The revision labels and outcomes below are examples of what to retain, not a customer execution record.
| Record | What the reviewer sees |
|---|---|
| Intent | SYS-REQ-041, revision R3: clamp requests to 1..20, preserving values inside the interval. |
| Candidate | Code revision C2; requirement R3; test revision T2; runtime and configuration recorded with the run. |
| Observed results | Boundary cases 0, 1, 20 and 21 passed in the example run. A real report would link the producing log with actual and expected values. |
| Unresolved gaps | Negative inputs have no observed result. Restart behavior was required by the plan but has not run. Both remain open. |
| Decision | Evidence incomplete for the declared plan. Acceptance pending the authorized decision; no merge or deployment is implied. |
Group routine passing checks, but disclose every failure, missing or stale result, disagreement, assumption and exception that could change the decision. A report can have zero open gaps or many. One attractive example must not hide the rest.
Generate a view of the recorded requirements
proof doc preview verification-report --format md
proof doc generate verification-report --output docs/verification.html
The current generator renders loaded project data into HTML or Markdown. Its verification report includes formalization, realizability, consistency, vacuity, review and trace-completeness information grouped by assurance level. It does not launch those analyses or refresh old results merely by rendering them.
Use the generated report as one input to the review package. Attach the producing executions, candidate revision, applicable policy and unresolved findings. Do not assume the template automatically supplies every field in the sample above. A field that lacks supporting evidence should remain unknown.
Inspect an actual package with a failed check.
The retained-obligation walkthrough runs the same five retry cases at three local Git commits. Reducing key retention from 24 to 12 hours produces duplicate reservations. Restoring 24 hours repairs the observed cases.
Proof executes the configured test command and assembles a package from each persisted run. The failing revision is blocked. Both passing revisions remain not_assessed: the packages retain missing change intent and requirement-level evidence, rather than treating a successful test command as acceptance.
Read the package and its companion results together.
The actual B package identifies the evaluated commit and two failed test cases. The executed case results record expected and actual reservation counts. The package’s evidenceRecords array is empty; those detailed results have not become traced per-requirement witnesses.
proof evidence package assemble --run <persisted-run-id> --base <base-ref>This command reads saved evidence and Git state. It does not run an audit. The downloadable example includes the exact command arguments, a real local Git bundle, source inputs and checksums. Its repository label is a reserved teaching identifier. No hosted PR or acceptance decision ran.
Use the reproducible setup to see the difference between a document rendered from project state and a sealed package tied to an observed run.
A new report can still contain an old result
Suppose last quarter’s report says a requirement is verified. The helper changes today, and the old test report remains on disk. Reprinting the row today does not show that the new helper was tested. Compare the result’s source, requirement and relevant configuration basis with the candidate, then rerun affected evidence.
A requirement amendment needs its own authority. If the implementation cannot satisfy the lower bound, changing the requirement to allow zero is a product decision, not a reporting repair. Proof retains requirements and their links so the current change can be assessed against earlier obligations.
See when evidence becomes stale for the basis to compare.
Use the report to make a scoped decision
Start with the behavior being changed and preserved. Follow each material claim to its evidence, inspect the open gaps, and apply the project’s approval policy. Agent-written checks can contribute when their oracle and execution support the approved intent. Required human review and independence obligations still apply.
A verification plan specifies the evidence to obtain; the report records what was obtained. An authorized acceptance decision records whether that evidence is sufficient for this revision. Program assurance documents and certifications may need additional records and responsible signoffs.
Bring one real change to a review workflow discussion, including its required checks and the gaps your reviewers currently reconstruct by hand.