The Proof Is Not the Architecture

Proof is Powerful Because it is Conditional

Formal methods offer something engineering badly needs: the ability to state claims precisely and determine whether they follow from explicit assumptions. Hoare’s axiomatic approach made this structure visible in program reasoning by relating preconditions, programs, and postconditions [Hoa69]. Lamport’s work on concurrent programs similarly showed how safety and liveness claims could be made precise for systems whose behavior cannot be understood from sequential execution alone [Lam77]. Formal specification and verification have since become important sources of evidence for critical systems [Rus95].

The familiar judgment

$\Gamma \vdash_L \phi$

says that the claim $\phi$ follows from assumptions $\Gamma$ under a logic $L$ . That is a strong statement. It is also a conditional one.

The judgment does not, by itself, establish that

$\Gamma$ contains every assumption relevant to the real system
The predicates in $\phi$ denote what engineers and stakeholders think they denote
The formal model preserves every architectural distinction needed by the claim
The modeled boundary includes every causal path capable of defeating the claim
The implementation realizes the model in a claim-preserving way
The operational environment continues to satisfy the assumptions

None of these observations invalidates the proof. But they do identify the boundary of what has actually been proved.

The Architectural Projection

Let an encountered architecture be denoted by $\mathcal{A}$ . As we’ve discussed in prior posts that architecture includes more than components and interfaces. It includes consequential decisions, causal dependencies, active obligations, assumptions, authority relations, retained evidence, prohibited behaviors, and the future possibilities still available from the present state.

Formal analysis does not operate directly on all of $\mathcal{A}$ . It operates on a projection of $\mathcal{A}$

$\pi: \mathcal{A} \longrightarrow M$

where $M$ is a formal model.

The projection is necessary. No useful model contains everything. Abstraction is one of the primary sources of formal power because it suppresses distinctions that do not matter to the claim being analyzed. The danger is not abstraction itself. The danger is failing to identify which distinctions were suppressed and whether one of them mattered after all.

A proof may establish

$M \models \phi$

where this is read as “ $M$ models $\phi$ .”

However, the desired architectural conclusion is usually closer to

$\mathcal{A} \models \hat{\phi}$

where $\hat{\phi}$ is the claim as interpreted over the encountered architecture. Moving from the first statement to the second requires more than a proof internal to $M$ . It requires a justified relationship among the

Architecture $\mathcal{A}$ ,
Projection $\pi$
Model $M$
Formal claim $\phi$
Architectural claim $\hat{\phi}$

This is where formal verification becomes an architectural problem.

A Precise Model Can Still Be The Wrong Model

We generally acknowledge that precision and accuracy are different concepts. We can be very precise and wildly inaccurate. We can also be accurate without being overly precise. However, engineering culture often treats increased formal precision as increased confidence. Within a fixed model, that is frequently justified. A more precise semantics, stronger invariant, or machine-checked proof can eliminate classes of ambiguity and error.

But precision and fidelity (or accuracy) are not the same property.

Michael Jackson’s problem-frame work emphasized that software problems must be understood through the domains and phenomena of the world in which the software acts [Jac01]. Leveson’s systems-theoretic safety work likewise argues that safety cannot be reduced to component reliability or isolated failure events. It depends on constraints and interactions across a larger control structure [Lev11].

A formal model may therefore be

Syntactically exact
Semantically well-defined
Internally consistent
Mechanically checked
Architecturally inadequate

This happens when the projection omits a distinction on which the real claim depends. For example, two events may be represented as equivalent because they produce the same local output, while differing in authority, timing, provenance, reversibility, or their effect on later decisions. The proof may be correct over the collapsed representation while the architectural claim fails in the richer system.

Formal precision can therefore amplify confidence in an insufficient projection. That is not a defect unique to formal methods. It is a general engineering hazard that becomes especially consequential when the formality of the result obscures the human choices that produced the model.

The Cognitive Architecture Beneath The Formal Architecture

Looking back over the entirety of this blog series, there is an underlying current: the influence of human cognition on the engineering process, including the ways cognition shapes what engineers notice, distinguish, preserve, suppress, formalize, and eventually treat as authoritative. This theme appears in discussions of architectural memory, encountered complexity, technical debt, metrics, decision order, representation fidelity, and the loss or preservation of future options. Formal methods do not sit outside that underlying current. They provide disciplined structures for reasoning, but the construction and use of those structures remain cognitive acts.

Formal models are often presented as though they remove human cognition from the engineering process. However, in practice, they relocate it.

People still decide

Where the system boundary lies
Which events are distinct
Which variables represent state
Which environmental behaviors are assumptions
Which claims are worth proving
Which uncertainties may be abstracted
Which counterexamples are meaningful
When the evidence is sufficient to permit commitment

These are not clerical steps to be performed before the “real” formal work begins. They construct the effective formal architecture.

Rasmussen’s distinctions among skill-, rule-, and knowledge-based behavior showed that human performance changes qualitatively with familiarity, context, and the structure of the task [Ras83]. Cognitive systems engineering later emphasized that performance emerges from a joint system of people, artifacts, automation, and work constraints rather than from isolated human or machine components [WH06]. Naur’s account of programming as theory building made a related point. The primary product of programming is not only text, but a theory held by the people who understand how the program addresses their problem [Nau85].

Formalization is also theory building. The engineer must form a theory of what matters, what may change, what can be ignored, and what must remain invariant. The formal notation records part of that theory, but it does not automatically record the cognitive path by which the theory was formed. Nor does it guarantee that another engineer can or will reconstruct the same interpretation from the same symbols.

The Program Has More Than One Order

Knuth’s literate programming makes this cognitive structure unusually explicit. A program need not be presented in the order demanded by a compiler. It can instead be organized so that concepts are introduced in an order more suited to human understanding, while tools are used to derive both executable code and coherent documentation from the same interleaved source [Knu84, Knu92].

This separates three distinct orderings that conventional source files often collapse

$\text{order of discovery } \ne \text{ order of expression } \ne \text{order of execution}$

The programmer may, and usually will, discover the solution nonlinearly, moving among abstractions, mechanisms, unresolved questions, and provisional fragments. The machine ultimately requires a valid executable ordering. A future engineer needs an explanatory ordering that supports reconstruction of the design theory. Literate programming mediates among these orders and preserves more of the cognitive architecture of the program than a linear source listing followed by retrospective documentation.

This does not preserve the entire thought process. False starts, tacit judgments, and rejected alternatives may still disappear. But it acknowledges that executable order is not the same as intelligible order, and that documentation should participate in the construction of understanding rather than merely describe the result afterward.

Reuse Without Recovered Theory

The same distinction exposes a limitation in fragment, library, and API reuse. A reused artifact may transfer executable behavior without transferring the theory that made the behavior appropriate in its original context. A code fragment, library call, or API operation may appear locally compatible while carrying hidden assumptions about timing, state, authority, failure recovery, concurrency, resource ownership, trust, or expected modes of change.

Interface compatibility is therefore weaker than architectural compatibility. A more complete reuse claim would require evidence of compatibility among behavior, assumptions, semantics, invariants, obligations, and architectural role. Empirical work on API usability confirms that learning and correctly applying an API is a cognitive engineering task rather than a trivial consequence of interface availability [PFM13].

This suggests two related principles

Source code, models, APIs, libraries, documentation, and proofs are artifacts produced by engineering cognition. None is identical to the theory held by the people who constructed and understood the original system in which those artifacts were created.
Reusing an implementation or formal artifact without recovering the assumptions, distinctions, obligations, evidence, architectural role, and design theory that produced it transfers structure while severing part of its architectural meaning.

Library and API reuse can improve reliability and productivity precisely because engineers do not need to reconstruct every internal detail. But abstraction does not remove the need for understanding. It changes the required level of understanding required. The engineer must still know enough to judge whether the abstraction’s guarantees, exclusions, side effects, and failure modes are compatible with the claims being made for the larger system.

Under schedule pressure, that reconstruction is often incomplete. Engineers, including experienced and conscientious engineers, may select a familiar library, imitate a usage pattern, or accept an API’s apparent contract without sufficient time to explore its boundary cases and second-order consequences. A systematic review of time pressure in software engineering found that increased short-term productivity is commonly accompanied by reduced quality and that knowledge mediates the effects of schedule pressure [KMF+20]. The issue is not simply haste in typing code. It is compression of the time available to build and test an adequate theory of what the reused artifact means in the new context and architecture.

Reflection is Engineering Work

This leads to a broader systems-engineering consequence. Good engineering requires time not only to produce artifacts, but to reflect on them, i.e., to reconstruct assumptions, trace interactions, compare alternatives, examine counterexamples, and consider consequences that are not visible at the local interface. Better engineers are distinguished partly by their willingness to pause for that work. Better engineering organizations are distinguished by their willingness to make that pause possible.

Reflection is therefore not overhead external to engineering. It is part of the work by which architectural understanding is constructed and preserved. When schedules eliminate reflection, they do not merely accelerate the same engineering process. They alter the process by suppressing a source of evidence and by encouraging commitments before their causal implications have been understood.

This gives us another useful principle

A formal model does not eliminate cognition from architecture. It makes selected products of cognition explicit while leaving other judgments embedded in modeling choices, notations, proof obligations, reuse decisions, and interpretation.

The cognitive contribution is therefore not external noise added to an otherwise pure formal process. It is part of the causal history of the proof, the program, and the architecture in which both acquire meaning.

Proof Excludes Modeled Counterexamples

A proof can establish that no counterexample exists within the represented state space under the stated assumptions. That is extraordinarily valuable. But counterexamples can also be absent because

The relevant behavior was outside the model boundary
The event vocabulary could not express it
An environmental assumption ruled it out
Two causally different situations were abstracted into one state
The property was weaker than the architectural obligation
The implementation introduced behavior not preserved by the model relation.

Long-running debates over program verification reflect different aspects of this boundary. DeMillo, Lipton, and Perlis emphasized the social processes by which proofs gain acceptance and meaning in mathematical practice [DLP79]. Fetzer argued that causal interaction with physical machines complicates claims that formal program proofs alone guarantee actual executions [Fet88]. Their strongest conclusions remain controversial, but the underlying architectural question is unavoidable

What relation connects formal objects to executing systems in an encountered world?

The right response is not to retreat from proof. It is to state the connecting claims explicitly.

What Must Accompany “Formally Proved”

The phrase “formally proved” is materially incomplete unless the engineering record also identifies at least

The formal claim and its intended architectural interpretation
The logic selected and admissible proof principles
The non-logical axioms and environmental assumptions
The model boundary and abstraction choices
The semantics of the modeling language
The relation between the model and the implementation
The evidence that this relation holds
The claim class preserved by that relation
The conditions under which the claim must be reconsidered

This is a logical-foundation disclosure requirement, but it is also an architectural memory requirement. Without it, later engineers inherit a proof artifact while losing the decision history that determines what the proof means.

Parnas and Clements observed that real design processes rarely follow the clean rational sequence later presented in engineering documentation, even though reconstructing a rational account remains valuable [PC86]. The same tension appears in formal work. The polished proof may conceal exploratory modeling, rejected abstractions, interpretive disputes, and changes in the claim. Those discarded paths are often where the architectural meaning resides.

Proof Validity, Model Adequacy, and Claim Applicability

It is useful to separate three questions.

Is the proof valid?
- Does $\phi$ follow from $\Gamma$ under $L$ , according to the stated semantics and proof rules?
Is the model adequate?
- Does $M$ preserve the distinctions, behaviors, and causal structure required for the claim being investigated?
Is the claim applicable?
- Does the encountered architecture, implementation, and operating context satisfy the conditions required to transfer the formal results?

A strong assurance argument needs all three. They demand different evidence and may fail independently. I would also argue that the third question is likely the hardest to answer.

A valid proof over an inadequate model does not establish the intended architectural claim. An adequate model with an invalid proof does not establish it either. And both may be sound while the implementation or environment violates the relation needed for application.

The Proof Is Not The Architecture

The title of this post is not an argument against formal methods. It is an argument against asking a proof to carry claims that belong to the architecture surrounding it.

Formal methods are strongest when they make their boundaries visible. A proof can tell us exactly what follows from a formal construction. Architecture must tell us why that construction represents the distinctions that matter, why its assumptions are credible, how its claims attach to the encountered system, and how those claims survive change.

The proof is not the architecture.

But a well-constructed architecture can carry proofs, assumptions, obligations, evidence, and preservation relations as part of its decision memory. When it does, formal methods become more than detached verification artifacts. They become durable components of architectural knowledge.

This is the direction of the posts that follow. The next question goes deeper than considering which proof was produced

How does the chosen logic help construct the architecture that can be formally seen?

References

[DLP79] Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271–280, 1979.

[Fet88] James H. Fetzer. Program verification: The very idea. Communications of the ACM, 31(9):1048–1063, 1988.

[Hoa69] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 583, 1969.

[Jac01] Michael Jackson. Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley, 2001.

[Knu84] Donald E. Knuth. Literate Programming. The Computer Journal, 27(2):97–111, 1984.

[Knu92] Donald E. Knuth. Literate Programming. Center for the Study of Language and Information. Stanford, California, 1992.

[KMF+20] Miikka Kuutila, Mika Mäntylä, Umar Farooq, and Maëlick Claes. Time Pressure in Software Engineering: A Systematic Review. Information and Software Technology, 121:106257, 2020.

[Lam77] Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, 1977.

[Lev11] Nancy G. Leveson. Engineering a Safer World: Systems Thinking Applied to Safety. MIT Press, 2011.

[Nau85] Peter Naur. Programming as theory building. Microprocessing and Microprogramming, 15(5):253–261, 1985.

[PC86] David Lorge Parnas and Paul C. Clements. A rational design process: How and why to fake it. IEEE Transactions on Software Engineering, SE-12(2):251–257, 1986.

[PFM13] Marco Piccioni, Carlo A. Furia, and Bertrand Meyer. An empirical study of API usability. In 2013 ACM/IEEE International Symposium on Empirical Software Engineering and Measurement, pages 5–14, 2013.

[Ras83] Jens Rasmussen. Skills, rules, and knowledge; signals, signs, and symbols, and other distinctions in human performance models. IEEE Transactions on Systems, Man, and Cybernetics, SMC-13(3):257–266, 1983.

[Rus95] John Rushby. Formal methods and their role in digital systems validation for airborne systems. Technical report, SRI International, Computer Science Laboratory, 1995.

[WH06] David D. Woods and Erik Hollnagel. Joint Cognitive Systems: Patterns in Cognitive Systems Engineering. CRC Press, 2006.