The engineering behind a trustworthy change

Less guesswork.
Better evidence.

Practical guides for the decisions software teams face: what to preserve, what to verify and what to do when the evidence is incomplete.

Start with the work in front of you.

01 / Agent-written changes

Know what you are merging.

Look beyond the diff. Connect the intended behavior to the checks that actually ran and the questions still open.

What to check before merging → Build a useful review brief →

02 / Existing software

Recover the promises worth keeping.

Separate accepted behavior from accidental behavior. Preserve the agreement through a migration or the next agent’s task.

Recover requirements from code → Plan a consequential migration →

03 / Verification and defects

Make the result inspectable.

Find the obligations your suite misses, challenge plausible code and retain the lesson after a fix.

Find untested promises → Read an evidence report →

04 / Assurance obligations

Connect engineering work to the review.

Identify the applicable source and scope, then prepare evidence without confusing a mapping with compliance.

US defense AI4SDLC guidance → Cyber Resilience Act scope → EU AI Act and software assurance →

Find a guide or a specific check.

Guides explain a practice and its trade-offs. Check references describe a particular Proof diagnostic, its trigger and how to address it.

Guide
A crash your suite missed is a new verification obligation.
First preserve the failure. Then find the missing condition, fix the instance and decide how much of the wider failure class needs checking.
Guide
A SOC 2 report and a pentest do not answer every product question.
Assurance depends on the scope of the assessment. Inspect what was examined before assuming it establishes the correctness of a particular business rule.
Guide
A software accomplishment summary should expose the basis for acceptance.
Summarize the released scope, lifecycle evidence, deviations and open issues with references a reviewer can follow. A polished document cannot repair missing evidence.
Guide
A software baseline gives a change a stable point of comparison.
Name the requirements and revisions you accepted, then make later changes explicit. A baseline is a reference for review, not a promise that everything in it is correct.
Guide
A software checklist should show the work behind the tick.
A useful checklist names the work, the evidence that completes it and what happens when that evidence changes. Start with one repeatable engineering process.
Guide
A software design document should explain the decisions the code cannot.
Document responsibilities, interfaces, important trade-offs and how the design satisfies requirements. Keep the links current as the implementation changes.
Guide
Acceptance criteria: examples you can use in Jira
Write testable acceptance criteria in Jira with a ready-to-use story template, Given/When/Then examples, and clear boundaries between criteria and test results.
Guide
AI writes the specs and code. Who verifies the intent?
Recovered intent is a candidate until authorized under project policy. Separate product decisions, implementation and observed evidence; inspect current approval defaults.
Guide
ARP4754A, ARP4754B and the software evidence underneath.
Keep the aircraft and system development basis distinct from software verification. Trace the allocated promise into the software evidence that supports it.
Guide
Ask the right question with formal methods
Separate satisfiability, realizability, model checking and source proof, with a concrete contract example and explicit evidence limits.
Guide
Build tests from requirements
Turn an approved behavioral promise into cases, assertions, and current execution evidence. Generated fixtures and trace annotations are only parts of that chain.
Guide
Characterization tests preserve observed behavior. Decide which behavior deserves preservation.
Capture what the existing system does, then separate accepted compatibility from accidental behavior before making it the contract for a replacement.
Guide
Check migration behavior through outputs and durable effects
Run an API migration comparison with actual SQLite effects. Inspect a rejected request that still writes data, permitted normalization and a recorded illustrative disposition.
Guide
Choose between a data proof, a contract check and a code lemma
Understand the different roles of SMT solvers, Kind2 contract analysis and Proof's supported source-lemma path.
Guide
Choose test inputs by the behavior they should share
Use equivalence partitions and boundary values to design meaningful tests without claiming one sample proves an entire class.
Guide
Clear technical English helps people read. It does not prove the requirement.
Use controlled language to reduce ambiguity in documentation, then separately check that the statement expresses the right behavior and has supporting evidence.
Guide
Connect a formal claim to the source it describes
Link requirements to source lemmas and tests while keeping trusted summaries and fingerprint freshness distinct from semantic equivalence.
Guide
Connect requirements to executable checks
Build an inspectable path from approved intent to models, tests, and current results without confusing executable checks with complete requirements.
Guide
Correctness and security audits ask overlapping questions.
Security examines threats and protections. Correctness examines whether intended behavior holds. A serious change can require evidence from both.
Guide
Create a requirements summary people can review
Generate a requirements summary from recorded state, explain its scope and status, and keep document generation distinct from fresh verification.
Guide
Critical design review (CDR): checklist and exit criteria
Prepare a critical design review with a software checklist, entry and exit criteria, and a worked failure-path example. Compare CDR with PDR and TRR.
Guide
Derive requirements that add useful detail
Refine stakeholder acceptance criteria into system responsibilities while preserving rationale, assumptions, authority, and verification obligations.
Guide
Describe what must happen over time
Read common linear temporal logic formulas, distinguish safety from liveness and recognize the limits of finite traces.
Guide
Design by contract makes caller and implementation obligations explicit.
State the conditions a caller must satisfy, the result a component promises and the invariants it must preserve. Then decide how each claim will be checked.
Guide
Do you need requirements management, a code reviewer, or software assurance?
Compare overlapping responsibilities, inspect the artifacts each workflow retains and choose a pilot based on the work your team repeats.
Guide
DO-278A: keep the CNS/ATM assurance basis explicit.
Ground-based aviation software has its own assurance context. Organize evidence around the applicable requirements and operating conditions, rather than relabeling an airborne checklist.
Guide
DO-333: a formal result needs a visible model and assumptions.
Formal methods can strengthen an assurance argument when the property, model and connection to the implementation are explicit.
Guide
Does the Cyber Resilience Act cover your software?
Work through CRA product scope, commercial supply, data connections, remote backends, exclusions and assessment routes. Includes a practical evidence worksheet.
Guide
Does the EU AI Act apply because an assistant wrote the code?
AI Act duties depend on the system, intended use and your role. Follow the classification sequence, amended application dates and engineering evidence map.
Guide
EN 50128 and EN 50716: which applies to your software?
Understand EN 50128, its EN 50716 successor, and how to record the applicable railway software standard for new development and maintenance changes.
Guide
Find failure sequences in a state model
Build a bounded, reviewable transition model and interpret model-checking results without extending them to an unmodeled system.
Guide
Find slow tests without removing the protection they provide.
Measure execution cost, identify what each expensive check establishes, then decide whether to optimize, move or selectively run it.
Guide
Gate an AI code change on its requirements
Design a requirement-aware CI gate with current evidence, protected intent, focused iteration, and explicit repository merge enforcement.
Guide
Give a fuzzer a failure it can recognize
Design deterministic fuzz targets with meaningful oracles, replayable inputs and bounded claims about executed behavior.
Guide
How do I analyze the impact of a software change?
Start with recorded requirement reach, investigate unlinked dependencies and execute the affected evidence. Graph traversal is not a proof of behavioral impact.
Guide
How do I connect hazard analysis to code and verified fixes?
Carry a hazard from exposure and disposition through mitigation, code, executed evidence and residual-risk acceptance. A catalog review is not a verified fix.
Guide
How do I know every requirement has code and test coverage?
Freeze the requirement inventory, inspect implementation and evidence links, and distinguish current passing observations from missing or deferred evidence.
Guide
How do I let AI agents ship faster without shipping more bugs?
Remove repeated investigation and verification work while keeping the acceptance standard explicit. Give the agent the relevant requirements, risks and prior failures before implementation, then carry the decisions forward and renew any evidence whose basis changes.
Guide
How do I turn a written spec into checkable obligations?
Translate intended behavior into inputs, assumptions, observable outcomes and evidence obligations. Model compilation, realizability and code verification remain distinct.
Guide
How do stakeholder, system and software requirements connect?
Decompose a stakeholder outcome into system behavior and owned software obligations. Preserve assumptions, authority, parent links and tests at each level.
Guide
How do we put AI4SDLC requirements and testing guidance into practice?
A practical AI4SDLC walkthrough: source, approved requirement, risk, implementation, executed checks, revision and unresolved evidence.
Guide
How do you recover requirements from an existing codebase?
Separate observed behavior from intended behavior, retain its sources, resolve conflicts and turn approved requirements into checkable obligations.
Guide
How to record an informed risk acceptance
Risk acceptance is an authorized decision to tolerate a stated failure mode under defined conditions. It should preserve the evidence, affected promises, containment and next review date so the decision can be revisited when its basis changes.
Guide
How to verify a change without trusting its author’s explanation.
Choose evidence whose expected result comes from an agreed requirement, then make the result reproducible on the reviewed revision.
Guide
How to verify a rewrite preserves business behavior
Verify a rewrite with explicit requirements, old/new comparisons and checks of durable effects. Use a practical acceptance checklist and a numeric boundary example.
Guide
How to verify AI-generated code before merge
Verify AI-generated code before merge with a six-step checklist, a free PR evidence worksheet and a real Omarchy regression, fix and recorded test results.
Guide
IEC 61508 software evidence starts with the safety function.
Identify the allocated software obligation and the conditions under which it must hold. Then connect the design, implementation and evidence to that claim.
Guide
IEC 62304 evidence should stay connected to the software change.
Medical-device software lifecycle records are easier to review when requirements, risk-related behavior, implementation and verification share an identifiable basis.
Guide
INCOSE Guide to Writing Requirements: a practical review
Use the INCOSE Guide to Writing Requirements with a worked rewrite, a review checklist and links to the official v4 guide and its characteristics summary.
Guide
Investigate inconsistent requirements
Distinguish conflicting intent from modeling mistakes, pairwise consistency from whole-model realizability, and counterexamples from confirmed implementation defects.
Guide
Investigate where two implementations disagree
Build a meaningful differential comparison, preserve minimized divergences and distinguish parity from correctness.
Guide
ISO 26262 software evidence needs an allocated safety requirement.
Connect the software change to the safety behavior it serves, then inspect the relevant implementation and verification under the project’s agreed scope.
Guide
ISO/IEC/IEEE 29148 is about engineering requirements, not just writing “shall.”
A useful requirement has a purpose, an authority, a clear boundary and a way to determine whether it holds. Manage those facts throughout change.
Guide
Keep a requirement's meaning through its lifecycle
Distinguish draft intent, review, approval, evidence freshness, deprecation, retirement, and supersession without erasing history.
Guide
Keep stakeholder intent authoritative
State stakeholder outcomes, acceptance criteria, constraints, and authority so system and software requirements preserve the intended product behavior.
Guide
Keep verification effort visible as delivery grows.
More changes, teams and agents increase the cost of reconstructing context. Scale the reusable agreement and evidence, then measure whether work actually disappears.
Guide
Make CI check the promises that changed.
A useful correctness gate connects a revision to its requirements and current evidence. It should explain failures and missing support, not just add another green badge.
Guide
Make combinations of rules visible with a decision table
Build a decision table that exposes missing and conflicting outcomes, then connect its reviewed cells to implementation evidence.
Guide
Make quality requirements measurable
Specify performance, reliability, resource, and security expectations with operating conditions and appropriate evidence, not only category labels.
Guide
Make requirement assumptions reviewable
Separate environmental assumptions from system guarantees, give assumptions owners and evidence, and revisit them when operating conditions change.
Guide
Measure MC/DC in Go without losing the requirement
Plan condition-independence cases, measure supported Go decisions, and inspect the runtime evidence while checking behavior missing from the decision itself.
Guide
Measure the evidence behind software quality metrics.
A number becomes useful when its denominator, scope, revision and decision are clear. Counts of tests, requirements or findings are not quality on their own.
Guide
Migrate a critical service with an explicit preservation contract.
Name the promises that survive the move, gather evidence at the boundaries and keep the cutover decision separate from implementation completion.
Guide
Modernize legacy software by recovering one useful agreement at a time.
You do not need a complete specification before making progress. You do need to distinguish intended behavior from the accidents you discover.
Guide
More agent-written code needs a better acceptance process.
If every generated change requires a senior engineer to reconstruct the system, faster code generation just creates a longer review queue.
Guide
Mutation testing: can your tests detect a broken requirement?
Run a Python mutation-testing example: two hand-applied mutants survive a weak test and are killed by requirement-derived assertions. Inspect the source and results.
Guide
NASA-STD-8739.8B: software assurance and software safety
Understand NASA-STD-8739.8B, its software assurance, safety and IV&V scope, and its relationship to NPR 7150.2D. Start with the project’s applicability basis.
Guide
NPR 7150.2D: NASA software engineering requirements
A practical overview of NPR 7150.2D: software classification, applicable requirements, lifecycle evidence and the relationship to NASA-STD-8739.8B.
Guide
Plan the evidence before the implementation is finished.
A software verification plan turns requirements and risks into specific checks, environments, acceptance rules and responsibilities.
Guide
Plausible code can implement the wrong promise.
Generated code often looks reasonable because it matches a familiar pattern. The useful question is whether that pattern fits your product’s actual obligations.
Guide
Preliminary design review (PDR): purpose and checklist
What a preliminary design review should establish, what to prepare, and how PDR differs from CDR. Includes a software architecture checklist and example.
Guide
Prove an invariant beyond a bounded search
Understand base and step obligations, unreachable step counterexamples and strengthening invariants in k-induction.
Guide
Replacing a system without specs or tests starts with observation.
Build a small, reviewable account of what must survive before asking a replacement to match a system nobody has described.
Guide
ReqIF moves requirements between tools. Verify what survives the move.
Requirements Interchange Format is an exchange format. Successful import is only the beginning of checking identity, content, relationships and authority.
Guide
Requirements traceability matrix: example and template
Download a free requirements traceability matrix CSV, inspect a filled example, and follow six steps to track requirements, test results and stale evidence.
Guide
Requirements-as-code: choose a workflow that survives change
A practical requirements-as-code buying guide covering StrictDoc, Doorstop, Sphinx-Needs and Proof. Evaluate authority, source links, evidence and migration work.
Guide
Resolve ambiguous requirements before choosing behavior
Turn vague requirements into explicit decisions about triggers, bounds, failures, and authority, with a worked retry example.
Guide
Review a requirement with its implementation evidence
Use a requirement-focused review to examine intent, lineage, assumptions, implementation, tests, drift, and authority before advancing a change.
Guide
Review requirement quality beyond a score
Combine automated record-quality findings with a substantive review of clarity, necessity, feasibility, boundaries, and evidence.
Guide
Review requirements completeness in layers
Distinguish complete records, connected hierarchy, allocated obligations, and complete product intent. Use structured scenarios to find what automated checks cannot.
Guide
Review the change, not just the diff.
A pull request needs a clear account of intended behavior, affected promises, current evidence and unresolved decisions. Code inspection is one part of that account.
Guide
Run a system requirements review with a clear decision
Review system requirements for accepted intent, consistent models, complete allocation, assumptions, and unresolved risks, using Proof's SRR evidence within its scope.
Guide
SARIF carries analyzer findings. It does not settle them.
Use the report to preserve where a tool found a potential problem, then connect that signal to a requirement, an investigation and a defensible outcome.
Guide
Scope a formal verification engagement around a decision
Define a bounded claim, reviewed assumptions, reproducible evidence and explicit unresolved outcomes for a verification engagement.
Guide
Select affected tests without pretending the graph is complete.
Test impact analysis uses known relationships to choose relevant checks. When those relationships are missing, the safe outcome is a broader run or an explicit gap.
Guide
Software requirements specification (SRS): template and example
Write an SRS with a reusable outline and worked software requirements. Cover behavior, interfaces, constraints, acceptance criteria and change control.
Guide
Software verification report: example and template
Build a software verification report with a reusable template, worked example and actual run artifacts. Record revisions, results, gaps and acceptance separately.
Guide
Software verification starts with a claim you can check.
Verification asks whether software meets specified requirements. Useful evidence identifies the claim, the method, the observed result and the exact version checked.
Guide
Specification conformance needs more than matching words.
To assess conformance, identify the authoritative requirement, the implementation behavior and the evidence that connects them for the reviewed revision.
Guide
Specify what rejection must leave unchanged
Design negative tests around exact rejection behavior, state preservation and real interface reachability.
Guide
State what remains true while a loop runs
Understand establishment, preservation, exit reasoning and termination using a simple scanning-loop example.
Guide
Test a rule across many generated examples
Design meaningful properties and input generators, preserve minimized failures and distinguish testing from universal proof.
Guide
Test readiness review (TRR): checklist and exit criteria
Prepare a test readiness review: candidate build, procedures, pass criteria, environment, evidence and anomaly handling. Includes a practical TRR checklist.
Guide
Track where untrusted values gain authority
Understand source-level taint analysis and distinguish it from Proof's scoped requirement-level trust checks.
Guide
Turn a privacy decision into a test that can fail
Turn an approved privacy decision into a testable engineering requirement. Inspect an executed two-store deletion failure, retry and restore example with source.
Guide
Use requirement diagrams to inspect relationships
Generate hierarchy, component, and impact diagrams from Proof's recorded data, then use them to review missing links and change reach.
Guide
Validate requirements before trusting their checks
Distinguish schema validation, model preflight, stakeholder validation, and implementation verification with a concrete workflow.
Guide
Verify the transaction, including what happens after a timeout.
Financial workflows need explicit promises about amounts, identity, ordering and recovery. A successful API response is only one observation.
Guide
What DO-178C can teach an agentic software team.
Requirements, traceability and disciplined verification are useful beyond aviation. Adopting selected practices does not make a product or tool DO-178C compliant.
Guide
What does a safe agentic development pipeline look like?
Start with approved intent, give the agent a bounded change and collect evidence against that intent. Acceptance, merging and deployment are separate transitions, each with its own prerequisites.
Guide
What does Cyber Resilience Act reporting require?
Understand CRA reporting triggers, the shared awareness clocks, separate final-report anchors and the engineering evidence a reporting owner needs.
Guide
What guardrails should I put around autonomous coding agents?
Control what the agent may change, what it may execute and what evidence allows the result to proceed. Keep these controls outside the implementation agent’s discretion, and make exceptions explicit.
Guide
What is integration testing, and how do I verify an interface?
Test the actual wired boundary, capture exchanges and outcomes, and distinguish integration annotations, execution results and enforced CI policy.
Guide
What is the difference between test coverage and requirements coverage?
Structural coverage counts code exercised. Requirements coverage counts declared obligations with evidence. State the denominator and distinguish linked tests from observed passes.
Guide
What should a software correctness audit deliver?
A useful audit investigates whether a bounded component meets its intended behavior. The deliverable is an inspectable case, including what was found, reproduced and left unresolved.
Guide
What should the next agent remember from a completed change?
A real scripted MCP retrieval and a proposed two-task agent experiment: retained draft intent, search limits and evidence that still needs renewal.
Guide
What should you check before merging an agent’s change?
Start with the promise the code must preserve. Then inspect the changed scope, executed evidence and remaining gaps, regardless of which coding assistant produced it.
Guide
When an agent silently breaks a requirement
Keep approved behavior authoritative across agent tasks, then use impact review, focused execution, and current evidence to detect regressions.
Guide
When does verification evidence go stale?
Compare a result with its relevant code, requirements, configuration, environment and policy. Renew the affected evidence without erasing history.
Guide
When the same area breaks again, keep more than the patch.
Recurring defects often expose a missing shared assumption, requirement or verification obligation. Investigate the pattern instead of treating each failure as unrelated.
Guide
Who checks the code when an agent wrote it?
Assign responsibility for intent, implementation, verification and acceptance. “Another AI reviewed it” does not answer all four questions.
Guide
Why do tests pass while bugs still ship?
Passing tests establish their assertions for the cases exercised. A runnable lower-bound example shows how a missing case survives a green suite.
Guide
Why do the same bugs keep coming back in our codebase?
A fix can disappear when the next change no longer carries the reason for it. Retain the original failure, the intended behavior and a regression check that fails without the fix. Keep them connected so the next engineer or agent can find them.
Guide
Write a requirement whose timing can be inspected
Use FRETish to make trigger, scope, timing and response explicit, then inspect compiled meaning and implementation evidence.
Guide
Write a software problem report that preserves the lesson
A useful problem report connects a failure to its cause, corrective work and evidence. It should let the next engineer distinguish a repaired instance from a broader recurrence-prevention claim.
Guide
Write an interface contract both sides can use
Define interface data, timing, failure behavior, assumptions, ownership, and evidence with a worked producer-consumer example.
Guide
Your suite can pass while a customer promise is untested.
A test suite is a collection of observations. Find the requirements it does not exercise before interpreting a green run as confidence in the whole change.
Check reference
Account for configured build targets
A result from one configuration should not silently stand in for every supported target. This check compares declared build targets with the configuration labels attached to collected test results.
Check reference
Allocate each stakeholder obligation to the system
obligation_completeness checks that eligible stakeholder checklist classes have active system satisfiers carrying the same classes.
Check reference
Anchor high-impact deployment claims
A high-impact claim needs a stated exposure or grading basis. This check distinguishes a recorded production-value anchor, an upheld external grade and a report that is still awaiting a verdict.
Check reference
Back a declared change type with evidence
The opt-in change_evidence_complete check validates refactor, fix, and feature backing on new impact reviews within its scoped Go change surface.
Check reference
Check a CLI command's contract footprint
contract_alignment_clean is a heuristic check for public Proof CLI files with too little requirement, help, or test coverage for their exposed surface.
Check reference
Check a delegated obligation has a real owner
obligation_delegation_resolves validates class and target IDs, target checklist ownership, rationale, cycles, and conflicting suppressions.
Check reference
Check a suppression's required reviewer record
obligation_suppression_reviewer requires reviewer identity for baseline suppressions meeting the configured severity threshold, but does not enforce reviewer independence.
Check reference
Check a system promise has a concrete realization
sys_has_software_child accepts an active software child or direct implementation/verification trace. An integration-only child does not satisfy this structural check.
Check reference
Check approval against the current requirement
An approval of an earlier requirement is not automatically approval of its edited form. This check compares the recorded approval with the current authored requirement under the project’s configured approval policy.
Check reference
Check closure evidence across declared platforms
When evidence says an issue no longer reproduces, ask which supported platforms were actually observed. This check identifies missing platform observations for that closure-relevant claim.
Check reference
Check declared interface coverage
interface_coverage finds gaps between declared components and interface requirements, with explicit no-interface attestations and external participants.
Check reference
Check documented ignore-trailer tokens
The opt-in description_grammar_enumeration_complete check compares Proof's MC/DC ignore-trailer tokens with their governing requirement description.
Check reference
Check model-verification continuity through a hierarchy
Understand exactly which recorded parent and child model results verification_chain_complete compares.
Check reference
Check obligation catalog integrity
catalog_completeness checks agreement between declared classes, catalog definitions, signal mappings, and requirement checklists. It does not measure complete intent.
Check reference
Check ownership across a component boundary
cross_component_clean checks declared cross-component requirements for component lists and child coverage, with explicit treatment of external parties.
Check reference
Check stakeholder requirements have system coverage
cross_level_complete checks that each eligible stakeholder guarantee has an active system requirement naming it in satisfies. Understand this precise structural scope.
Check reference
Check that child domains refine their parent
Use z3_cross_layer_consistency to inspect implication, coverage and overlap across comparable data-constraint domains.
Check reference
Check that the closure platform can reach the defect
A non-reproduction on a platform that cannot execute the affected path is weak closure evidence. This check makes that distinction explicit for issues declaring platform constraints.
Check reference
Check the contract's variable boundary before solving it
Use variables_declared preflight to catch missing declarations and ownership problems before model analysis.
Check reference
Check the contracts behind assumptions
Find unsupported or mismatched reqproof:assume contracts before relying on a caller's lemma.
Check reference
Check the evidence behind a defect disposition
A defect report should retain what changed, why the problem escaped and how the chosen disposition is supported. This audit checks the structure and cross-artifact basis of those records.
Check reference
Check the evidence required by each obligation
obligation_evidence_complete checks typed evidence cells, including nominal defaults and the execution provenance required for lemma, race, and fuzz evidence.
Check reference
Check the role of an acceptance witness
An acceptance annotation can point to the wrong kind of code. This check examines the tagged carrier so a production function or an ordinary derived test is not silently treated as stakeholder-level evidence.
Check reference
Check the shape of requirement levels
levels_connected checks configured level population, missing system layers, and component-level software-to-system links. It is not a complete graph reachability proof.
Check reference
Check the system requirement record
l1_system_complete checks active system records for a description, a satisfies link, and FRETish when that formalization strategy is explicitly selected.
Check reference
Check what modeled predicates actually imply
Interpret universal data-domain implication results separately from realizability, translation failures and implementation evidence.
Check reference
Check whether a lemma still names the current source
Detect target and lemma fingerprint drift in persisted separate-file bindings without confusing freshness with semantic equivalence.
Check reference
Check whether a requirement actually constrains behavior
Investigate vacuity and unchecked results before treating a successful model analysis as meaningful evidence.
Check reference
Check whether a witness reaches its implementation
obligation_witness_grounded uses static references and isolated coverage to inspect obligation witnesses, with explicit exemptions and unavailable-coverage results.
Check reference
Close gaps and overlaps in data partitions
Interpret data_constraints_complete results for authored input partitions and distinguish counterexamples from parse gaps or timeouts.
Check reference
Connect a change record to requirement review
change_record_lands checks that requirements named by change and defect records exist and cite those records in current or historical review motivation.
Check reference
Connect code signals to reviewed obligations
A code signal identifies behavior that may need a requirement, a check or a reasoned exception. This reference explains how Proof connects those signals to the requirement family responsible for the code.
Check reference
Connect documented claims to inspectable evidence
An API comment or user guide can promise behavior the implementation does not deliver. This check validates explicitly recorded claim-evidence cells so the promise has a place for implementation and verification references.
Check reference
Connect generated scenarios to verifying tests
Interpret legacy FLIP-to-test alignment findings and turn named scenario gaps into meaningful source tests.
Check reference
Connect obligation classes to evidence profile results
Check required normalized evidence-profile results, their requirement joins, and missing or failing producer output with obligation_profile_evidence_complete.
Check reference
Connect requirements to documentation
A requirement may be implemented and tested while its user-facing explanation remains missing. This check inventories documentation links for active requirements and applies the project’s configured documentation boundary.
Check reference
Connect software requirements to a live system parent
l2_software_complete resolves active software and integration requirements' satisfies targets to at least one active system requirement.
Check reference
Connect tests to the promises they examine
orphan_tests_clean identifies tests without recognized requirement ownership. Understand per-test annotation scope, imported suites, and evidence limits.
Check reference
Detect interface implementation drift
interface_staleness_clean compares implementation content hashes with the last interface review. Understand stale findings and the limits of legacy unstamped reviews.
Check reference
Explain why a requirement was reapproved
Reapproval should leave a reason that a later reviewer can inspect. This check validates the motivation record on recognized reapprovals and catches malformed motivation blocks on initial approvals.
Check reference
Explain why an obligation does not apply
obligation_suppression_rationale checks the presence and configured minimum length of reasons on active requirements' obligation suppressions.
Check reference
Find code without requirement ownership
Understand orphan_code_clean under source-native and overlay-audit trace policies, including function scope and the limits of a traced-only scan.
Check reference
Find data constraints the solver did not check
Compare authored data constraints with the variables reached by the Z3 property pipeline, including skip reasons and auxiliary scope.
Check reference
Find inputs with no specified output
Use gaps_clean to inspect unconstrained outputs, declared domain assumptions and bounded state enumeration.
Check reference
Find obligation classes with no enforcement backing
obligation_enforcement_backed flags cataloged checklist items with neither signal-rule backing nor evidence for the requirement/class pair.
Check reference
Find overlapping interface contract records
interface_contract_duplicates groups active integration requirements by normalized callee and signature. Review overlaps before consolidating contract history.
Check reference
Find requirements that demand incompatible outcomes
Understand the shared-trigger and mutex patterns checked by cross_spec_consistency_clean.
Check reference
Find requirements thinner than their evidence
Investigate model-depth warnings using requirement variables, witness density and code decision structure without mistaking counts for correctness.
Check reference
Follow obligations into children or implementation
obligation_decomposition_complete checks each parent's obligation allocation and requires an implementation trace for an obligation-bearing leaf.
Check reference
Follow up an overdue upstream issue
An upstream report needs a follow-up loop while the outcome remains unresolved. This check surfaces scheduled rechecks that are overdue instead of relying on someone remembering the disclosure.
Check reference
Formalize behavior at component boundaries
Check FRETish formalization for review and approved guarantees in configured cross-component layers.
Check reference
Give each investigation a traceable disposition
An investigation should end in evidence, owned follow-up work or an explicit deferral. This check connects non-terminal vector campaigns to those recorded outcomes.
Check reference
Give high-severity hazards an investigation owner
A high-severity obligation hazard should not disappear between requirement review and investigation planning. This check identifies authored hazard classes with no linked vector campaign.
Check reference
Give investigation concerns a disposition
A concern records something worth investigating before it is a confirmed KnownIssue. A review deadline keeps an unresolved hypothesis from disappearing into an indefinite backlog.
Check reference
Give nonboolean inputs a domain the model can inspect
Model numeric and enum inputs using ranges, data constraints or table values, with explicit auxiliary scope and enumeration limits.
Check reference
Give software requirements enough formal detail
Find missing or incomplete FRETish guarantees in configured formal layers beneath a formal parent.
Check reference
Give system requirements an upward trace
system_requirements_linked checks whether active system records have satisfies entries. Review the actual stakeholder relationship beyond that presence check.
Check reference
Ground high-stakes findings in a reproducer
A high-stakes finding needs more than a plausible narrative and a severity label. This check enforces a structural evidence floor for active issues claiming high impact or a possible exploit surface.
Check reference
Identify structurally unsupported severity claims
A high or critical label should have a stated basis. Proof’s severity-inflation policy flags two narrow record shapes that suggest a claim needs closer review.
Check reference
Investigate slow proof slices with comparable measurements
Interpret solver_latency_clean thresholds, recorded timing scope and contention-aware skips before changing proof boundaries.
Check reference
Keep a reproducible path to the finding
A stale test selector can run no relevant test while appearing successful. This check asks whether an active KnownIssue still has a usable reproducer reference.
Check reference
Keep a requirement's retirement record
deletion_without_retirement compares baseline requirement IDs with the current corpus and reports disappeared requirements. Preserve lifecycle records when retiring intent.
Check reference
Keep an issue linked to the relevant port
A mirror link says which source-to-target relationship an issue concerns. This check finds declared links whose resolved requirement scope does not overlap the issue.
Check reference
Keep bounded risk dismissals inspectable
A residual record preserves why an investigated angle falls below a stated threshold within a sampled domain. This check looks for missing samples, broken links and conditions that should reopen that conclusion.
Check reference
Keep code-signal suppressions reviewable
Suppressions can hide the same signal across many files. This check makes broad, expired or unexplained project-level exceptions visible before they become forgotten policy.
Check reference
Keep defect-claim reviews current
A review stamp is useful only while its reviewed inputs and outstanding claims remain accounted for. This check follows the defect-claim lifecycle from a missing review to unresolved or unpromoted findings.
Check reference
Keep derived trace links current
Read autolink_clean findings, repair source annotation scans, and understand what a clean trace refresh can and cannot establish.
Check reference
Keep formal components within a reviewable proof budget
Interpret proof_complexity_clean budgets and simplify or decompose models along real architectural boundaries.
Check reference
Keep formalization status honest about lemma results
Detect valid formalization claims backed by cached unknown, timeout, translation-error or solver-crash lemma verdicts.
Check reference
Keep investigation records and links valid
Campaign status is useful only when its fields and linked work can be inspected. This check validates the vector record’s structure and references.
Check reference
Keep required scenario fixtures present
Configure and repair missing FLIP fixtures without mistaking generated scenarios for executed test evidence.
Check reference
Keep review prompts focused on evidence
A review instruction that rewards zero findings can distort the investigation. This check searches installed role prompts for specific language that treats an empty result or a finding quota as the goal.
Check reference
Keep review roles connected to real resources
A role can tell an agent to run a check or consult a document that no longer exists. This check identifies broken role references before those instructions become an unreliable investigation plan.
Check reference
Keep severity prose and metadata aligned
Readers and automation should not receive conflicting grades for the same finding. This check compares a clearly stated prose grade with the issue’s structured severity.
Check reference
Keep sibling defects visible when one issue closes
Fixing one instance should not erase related open work. This check asks whether a fixed KnownIssue has accounted for its recorded sibling issues and listed sites.
Check reference
Keep system requirements available to formal analysis
Check active system requirements for the required FRETish strategy and nonempty formalization, with honest limits on what completeness establishes.
Check reference
Link a known issue to the promise it violates
A finding becomes easier to investigate and reuse when it names the requirement it contradicts. This check finds active KnownIssues that have no such anchor.
Check reference
Make a known issue useful to the next investigator
A title alone does not tell another engineer how to reproduce, assess or fix a problem. This check inspects the evidence, origin and supporting fields that make an active KnownIssue actionable.
Check reference
Make MC/DC exclusions explain their impact
Classify code ignores and honored witness exemptions, with explicit treatment of capability gaps and tracked known issues.
Check reference
Make the reproducer’s intent explicit
A test that preserves defective behavior can be useful characterization, but it should not masquerade as a test of the intended contract. This check flags one recognizable form of that ambiguity.
Check reference
Make unopened P0 investigations visible
A high-priority investigation can remain untouched while unrelated checks pass. This reference explains the narrow state that Proof’s unopened-campaign check reports.
Check reference
Model the decisions the code actually makes
Use code_predicates_modeled to find numeric decisions absent from a requirement model and document intentional exclusions.
Check reference
Move decision domains out of prose
Recognize enumerable domains that a requirement describes but its referenced variables do not model.
Check reference
Prepare a finding for external review
Before a finding goes outside the project, its assumptions and evidence need a reviewable record. This check surfaces missing submission-validation fields and conflicts with the recorded claim.
Check reference
Read coverage against the right requirement set
Interpret coverage_threshold using fresh imported coverage, the configured threshold and the chosen baseline scope.
Check reference
Read the actual result of a property proof
Interpret z3_properties_verified for modeled variable properties and data constraints, including accepted known-issue debt.
Check reference
Reaffirm a mirror after content changes
mirror_stale compares source and target file-set hashes with an authorized reaffirmation record. Parity of annotations alone does not establish equivalent behavior.
Check reference
Reconcile a requirement's variable list with its formula
Use variable_drift to find missing and stale authored variable-list entries relative to parsed FRETish.
Check reference
Reconcile a severity label with its CVSS vector
An issue should not silently carry a low severity label alongside a vector that computes to a higher band. This check asks for a consistent record or an explicit reviewed reason for the difference.
Check reference
Reconcile approved guarantees with known issues
An approved guarantee and an active issue affecting that guarantee deserve to be reviewed together. This check highlights that tension when the issue has no nonblocking release disposition.
Check reference
Reconcile security naming with security metadata
A finding named as a credential leak or cross-tenant defect should carry a corresponding assessment, or explain why that name does not imply security relevance. This check surfaces the mismatch.
Check reference
Record a treatment for security-relevant issues
A security finding should explain how exposure is contained or how the defect will be corrected. This check flags active records that provide neither treatment.
Check reference
Regenerate fixtures when their model changes
Check generated fixture freshness only for explicitly configured evidence components and regenerate the affected fixture class.
Check reference
Remove cycles from requirement dependency links
circular_deps_clean detects loops in the analyzed requirement relationships. Inspect the intended dependency direction instead of changing links to silence a cycle.
Check reference
Require property examples only where they are used
Configure optional Z3-derived property fixtures and distinguish their presence from a property proof or implementation test run.
Check reference
Resolve proposed catalog classes
A signal can propose an obligation class that the catalog does not contain yet. This check separates a real catalog gap from a proposal that is already available locally or in the shipped catalog.
Check reference
Resolve variables with no requirement to explain them
Investigate declared-unused and undeclared-used variables with component ownership and honest auxiliary exemptions.
Check reference
Retire bug-dependent exceptions after a fix
A coverage exception or obligation deferral may be justified by a live known issue. When that basis changes, the exception needs to change too. This check reports dispositions that outlive the defect they cite.
Check reference
Review acceptance criteria before relying on them
Acceptance criteria can be present yet too vague to guide a decision. This check asks for an explicit review disposition and flags a common testing slogan that hides the actual outcome.
Check reference
Review check exceptions before they expire
A waiver is an explicit exception to a check result. Keeping its reason, scope and expiry reviewable prevents a temporary exception from silently becoming the project’s normal behavior.
Check reference
Review code changes against requirement intent
What authored_delta_expected checks when traced source changes: current artifact and requirement fingerprints, impact reviews, and limits of an unchanged-intent decision.
Check reference
Review deadline and timelock casts
A narrowing conversion near a deadline deserves a specific investigation. This check identifies cached signal reports that combine deadline or timelock language with a narrow integer conversion and still lack a terminal campaign disposition.
Check reference
Review known issues on a usable cadence
An unresolved issue needs periodic reassessment, and an explicit release block needs a decision. This check identifies those records without presenting every current known issue as a new finding.
Check reference
Review new Go API surface in a refactor claim
An opt-in check flags new exported Go symbols that lack requirement backing when an impact review claims no authored change.
Check reference
Review obligation catalog upgrades
Use catalog_version_pinned to inspect the relationship between a project's catalog pin, the shipped catalog, and its configured upgrade policy.
Check reference
Review prose changes against formal intent
description_delta_reviewed checks description changes that leave a requirement's FRETish unchanged. Decide whether the edit clarifies or changes the promise.
Check reference
Review semantic catalog suggestions
How catalog_semantic_bindings_reviewed resolves advisory requirement-to-class matches against live bindings or reasoned rejections.
Check reference
Review the answers inside a PoC checklist
A proof-of-concept checklist can exist while every answer remains false. This check exposes unsatisfied general checklist rules on active high or critical KnownIssues.
Check reference
Review the obligations activated by requirement tags
obligation_baseline matches catalog tag predicates and checks whether applicable classes are accepted, suppressed, or validly delegated.
Check reference
Review trace links after either side changes
suspect_clean compares requirement and linked-target fingerprints with reviewed state, so changed evidence relationships reopen for review.
Check reference
Review what a proof of concept actually demonstrates
A proof of concept should reach the claimed behavior under stated conditions and include a meaningful control. This check makes the recorded quality review inspectable before a consequential finding is relied on.
Check reference
See which branches lemma translation reaches
Read lemma_branch_coverage as translator reach, with production scope and meaningful proof claims kept separate from executed test coverage.
Check reference
Spot lemmas that only restate their model
Use trivial_lemma as a syntactic review aid for identity, constant and body-substitution claims, with explicit heuristic limits.
Check reference
Track related sites while investigating a defect
A useful finding should prompt a bounded search for the same failure shape elsewhere. This check keeps the declared class, candidate sites and differentiation notes from remaining empty.
Check reference
Valid requirement annotations
Understand Proof's annotation_validity check: requirement IDs, obligation classes, evidence types, and the source locations that can carry each claim.

Put the ideas to work.

Bring a change you are not comfortable trusting yet. We will start with its intent and the evidence it needs.

Bring a change ↗

Choose a workflow. Inspect its evidence.

Compare requirements-as-code approaches, inspect Proof and Kosli, or start with a runnable change example. Each route keeps the scope, recorded observations and remaining gaps visible.

Browse all comparisons →