When a Correct Checker Validates an Incomplete Model

A development agent can produce a design, a model of that design, and checks against the model. If all three inherit the same omission, a passing check can leave the most important question unanswered: does the model represent what the agent actually built?

A checker cannot find a missing flow if the model gives it no way to represent that flow. The result may be correct within the model while the broader engineering claim remains unsupported.

In the first article, we translated an invented reporting requirement into explicit obligations: every transfer of protected reporting data needs authorized endpoints and an encrypted channel. Now we examine whether the design model captures the transfers that matter.

This worked example describes expected reasoning, not a recorded solver run. It illustrates where formal verification and AI-assisted critique can help, and what neither establishes alone.

Begin with a useful design and a narrow claim

The initial design contains a reporting service and a reporting store. Its model includes their connection, authorization conditions, and encryption requirement.

A bounded formal check can search for a violation among the situations represented within its declared scope and assumptions. For example, a model might be checked up to a stated number of components and transfers. Finding no counterexample within that bound is narrower than establishing that the deployed system satisfies the requirement.

The claim should identify the property checked, the model version, the assumptions, and the search bounds. It should also say whether the modeled design is possible at all. Contradictory assumptions can leave no situations to examine.

Reviewers need to distinguish a meaningful check from a result with nothing relevant to examine. The report should make its scope and assumptions understandable without requiring the reviewer to reconstruct the model.

Do not assume the conclusion into the model

Suppose we constrain the model so that every transfer is authorized, then ask whether an unauthorized transfer exists. A negative answer follows from that constraint. It does not establish that authorization was checked against an actual design.

A requirement describes what the design must satisfy. Evidence establishes whether the actual design satisfies it. Treating the requirement as an already established fact can make the review confirm its starting assumption.

For a validation example, make sure the candidate design can be represented even when it violates the property under examination. Include an ordinary valid case and a deliberately violating case, and check that the model permits meaningful situations. These checks help expose a self-confirming example; they are not a proof of model completeness.

Ask what the first model left out

Now a reviewer notices that the reporting service also sends diagnostic records to a support archive. The first model represented only the primary reporting connection.

An AI assistant can help generate questions: can diagnostic records contain protected reporting data? What about retries, exports, or administrative tools? Which evidence would establish the archive's authorization? These are review prompts, not findings until checked.

In our synthetic case, inspecting the design reveals a diagnostic flow carrying protected records. The archive has not been authorized to receive them. That provides a specific violation of the invented rule. If its contents or permissions were instead unknown, the correct next step would be investigation rather than a claimed violation or pass.

Challenge shared assumptions across the agent’s outputs

Imagine the development agent adds a diagnostics library while implementing the reporting service. Its architecture summary describes the main reporting connection but leaves out the library's export to the support archive. A model generated from that summary can repeat the omission. Checks derived from the same account may never ask about the export.

This is a risk to investigate, not a claim that all agents behave this way. The important point is that apparently separate outputs can share an evidence gap. Having another agent review the same incomplete summary does not, by itself, provide an independent view of the system.

Give the review a route back to implementation evidence: the actual dependency change, configuration, and relevant observed behavior. Compare those with the claimed data-flow boundary. An AI reviewer can help identify discrepancies, while responsible owners establish whether the evidence supports the finding and what the design must change.

Keep the roles distinct. Tests examine specified behavior. Bounded formal checks examine modeled properties. Critique challenges the scope and assumptions. Human review reconciles those results with the applicable obligations. Agreement among them becomes useful when reviewers can inspect their support and understand what each leaves unexamined.

Reconcile the finding with the design

Add the diagnostic flow to the model because evidence establishes that it exists. Then decide how the design should address it. The team might remove protected content from the diagnostic output or use an appropriately authorized destination. Either choice needs supporting evidence; renaming the output “sanitized” does not establish what it contains.

Update the model and the claims extracted from the revised design, then check them against the applicable obligations again within the declared bounds. Reconcile disagreements between the model, the design description, and observed behavior. If the checker rejects a design, the cause may be a real violation, a mistaken translation, or an incorrect modeling assumption. Fixing the model until it passes without resolving that distinction would lose the value of the exercise.

The reviewer should see the changed design, the finding that prompted it, the new check's scope, and the unresolved coverage questions together. AI critique can propose omissions, but it can also miss them or invent irrelevant ones. Evidence and accountable human review remain necessary.

Make the boundary part of the conclusion

A useful assurance statement says which property is supported, for which design, by which evidence, and with which limitations. It does not convert a bounded result into a blanket safety or compliance guarantee.

Formal checks in AI-assisted design review already have public precedents, including AWS's engineering-design discussion. The practical question is how well the complete review process connects the model to the system and challenges omissions.

For the next agent-generated change, compare the implementation diff with the design summary and the model used to check it. Name one flow or dependency that could be absent from the agent’s account, then investigate it. Assurance depends on that connection to the actual work, as well as the correctness of the checker. Next: when an approved decision should be reconsidered.