When Does a Proof Survive Implementation?

Part 3 of this series ended with a formally justified representation and an unfinished engineering problem.

Suppose we have selected an appropriate logic, stated an architectural claim, constructed a model, declared its assumptions, and established the desired properties. Suppose further that the proof is valid and that the model is adequate for the claim.

But, we still do not have the system as built, deployed, and encountered in use.

Between proof of acceptable system properties and operation of that system lie design decisions, source code, generated code, compilers, linkers, hardware, configuration data, networks, sensors, actuators, operators, maintenance actions, and an environment that does not necessarily behave like a formal variable. It’s tempting to treat all of this as one final step called “implementation”.

That word hides too much.

Implementation is not a single movement from an abstract object to a concrete one. It is a chain of transformations, each of which may preserve some claims, weaken others, invalidate others, or make them inapplicable.

The central question of this final part is therefore

Under what conditions does a formally established claim survive refinement, realization, deployment, and situated use?

The answer is not that every implementation must resemble its formal model in every respect. Nor is it that formal proof loses its value when physical realization begins. The answer is more exact

A proof survives implementation only through a claim-relative chain of preservation obligations, supported by evidence at every transformation where the claim can change meaning or applicability.

That formulation makes refinement central. It also makes clear why refinement alone is not enough.

Implementation Is a Chain, Not an Event

A development is often summarized by a refinement arrow such as

$\text{specification} \rightarrow \text{implementation}$

For many systems engineering claims, the actual chain is closer to

$\text{purpose} \to \text{architectural understanding} \to \text{formal representation} \to \text{design} \to \text{source program} \to \text{executable image} \to \text{configured system} \to \text{deployed system} \to \text{situated operation}$

This particular chain is appropriate for software intensive systems, but the same notion is true for any engineered system. You should note that the arrows are not interchangeable or commutative.

Moving from an architectural model to a design is not the same kind of transformation as compiling source code. Compiling source code is not the same as installing an executable on particular hardware. Deployment is not the same as operation under environmental, organizational, and human influence. And, yes, it’s obvious that these are different activities, but they also differ in their semantic underpinnings, applicable logics, and desired properties.

Each stage introduces different evidence and different possible failures.

A design refinement may require a simulation relation or invariant proof
A code transformation may require semantic preservation, verified compilation, or translation validation
A deployment step may require configuration control, hardware conformance, interface verification, and timing evidence
An operational claim may require calibration, monitoring, procedural compliance, maintenance evidence, and confirmation that environmental assumptions continue to hold

The lifecycle treatment in ISO/IEC/IEEE 15288 is relevant here because it does not collapse conception, development, production, utilization, support, and retirement into one undifferentiated realization event [ISO23]. The distinction between an architecture and an architecture description in ISO/IEC/IEEE 42010 is equally important: an architectural representation may guide realization without becoming identical to the entity realized [ISO22].

This suggests a related principle

Implementation-Chain Principle

Implementation is a sequence of heterogeneous transformations rather than a single terminal step. Assurance must be attached to the individual transformations through which an architectural claim moves.

If a claim crosses six transformations, confidence in five of those transformations does not repair an unjustified sixth.

Refinement Is a Relation, Not a Label

We frequently use the word refinement informally to mean that a later model contains more detail than an earlier one. However, more detail is not sufficient.

A concrete description can contain more detail and still violate the abstract description. It can introduce new behavior, remove an essential option, change the meaning of an event, weaken an obligation, or depend on an assumption that the abstract model did not contain. Formal refinement gives the word “refinement” a stronger meaning.

Let $A$ be an abstract specification and $C$ a more concrete specification. We can write

$C \preceq_{\rho} A$

to mean that $C$ implements $A$ according to some stated refinement or abstraction relation $\rho$ . The direction of the symbol is conventional. The important point is that the relation must be defined.

In a behavior-oriented formulation, one common requirement has the shape

$\rho(\text{Beh}(C)) \subseteq \text{Beh}(A)$

where $\rho$ maps concrete behaviors into the vocabulary of the abstract model.

We have just written the refinement relation as $C \preceq_{\rho} A$ . In isolation, this notation is legitimate because it orders specifications according to behavioral containment. Within the overall blog series, however, $\preceq$ has already been used to express causal precedence between events. Reusing it for refinement creates a semantic collision, i.e., a local definition distinguished the relations formally, but it did not prevent the established causal interpretation from being carried into the new expression. So, while the notation is mathematically permissible, it is representationally inadequate.

This is a small example of a larger, and important, formal methods problem. Formal symbols are not interpreted in isolation. Their prior use, surrounding theory, relational properties, and direction all contribute to their meaning. A formally declared notation can therefore remain semantically ambiguous within the larger body of reasoning in which it appears. For the purposes of this blog series and to alleviate this semantic ambiguity, we will replace the above notation with the more explicit notation

$\mbox{Refines}_{\rho}(C, A)$

In a state-based development, $\rho$ may relate concrete states to abstract states. Simulation obligations then show that initial states correspond and that concrete steps can be matched by appropriate abstract behavior. Data refinement develops this idea through abstraction relations and simulation proofs [dRE98]. Forward and backward simulations give related machinery for concurrent systems [LV95], while refinement mappings provide an influential account for state machine specifications containing safety and liveness requirements [AL91].

Event-B makes refinement a development discipline. Abstract events, states, and invariants are elaborated through more concrete machines, with proof obligations used to establish that the refinement is legitimate [Abr10].

These methods differ in detail. What they share, though, is the refusal to infer correct implementation from resemblance, traceability, naming, or intent. The relation does the technical work.

But even a valid refinement result remains relative to what the relation observes and preserves.

If $\rho$ hides time, that relationship cannot transfer a deadline by itself
If $\rho$ identifies two authority states, it cannot preserve a claim whose truth depends on the difference between them
If $\rho$ forgets resource consumption, it cannot establish a resource bound
If $\rho$ maps only individual executions, it may be inadequate for a security claim relating several executions
Hyperproperties such as noninterference require reasoning over sets of traces rather than merely one trace at a time [CS10].

Refinement therefore never preserves everything. It preserves a claim class under a stated interpretation. This leads us to another useful principle

Claim-Relative Refinement Principle

A refinement relation is architecturally adequate only relative to the class of claims, distinctions, observations, and obligations it has been shown to preserve.

The statement

“The implementation refines the model”

is consequently incomplete until we know the relation, its semantics, its observables, and the claim class for which preservation follows.

The Claims Must Move as the Model Moves

Suppose an abstract model $M_0$ satisfies property $\varphi_0$

$M_0 \models \varphi_0$

Development produces a sequence

$M_0 \xleftarrow{\rho_0} M_1 \xleftarrow{\rho_1} M_2 \leftarrow \cdots \xleftarrow{\rho_{n-1}} M_n$

where each $M_{i+1}$ is more concrete than $M_i$ . We can easily imagine that the same sentence $\varphi_0$ simply follows the models downward.

Usually it does not.

The abstract claim must itself be interpreted at every stage. Let

$\tau_i : \varphi_i \mapsto \varphi_{i+1}$

represent the translation of the claim into the vocabulary and semantics of the next representation. Then a preservation step has at least two parts

The concrete artifact must relate correctly to the abstract artifact under $\rho_i$
The target claim $\varphi_{i+1}$ must be an adequate interpretation of $\varphi_i$ under $\tau_i$

This is the realization counterpart of the translation problem introduced in the preceding posts. Syntax can change while meaning is preserved. Syntax can remain nearly identical while meaning changes.

For example, the variable safe may mean

Membership in a formal state set
Completion of a software transition
Issuance of a command to an actuator
Measured attainment of a physical condition
An operator’s determination that continued operation is acceptable

Those are not interchangeable propositions.

If the implementation sets a Boolean variable named safe, the name does not establish that the physical system is safe. Claim transfer requires an interpretation connecting the propositions.

A useful schematic rule is

$\frac{M_i \models \varphi_i \quad E_i \vdash \text{Preserve}(\rho_i, \tau_i, \mathcal{C}_i) \quad \varphi_i \in \mathcal{C}_i}{M_{i+1} \models \varphi_{i+1}}$

where $E_i$ is the evidence for the refinement and claim translation, and $\mathcal{C}_i$ is the preserved claim class.

The above display of the schematic rule uses Gentzen inference-rule notation familiar from natural deduction in which the judgments above the line are premises, and the judgment below is the conclusion licensed or accepted when those premises are established [Gen35, Gen69, Pra65]. A premise may be an undischarged assumption, an axiom or initial judgment supplied by the theory, or the conclusion of an earlier accepted rule. Natural deduction is distinguished less by rejecting axioms than by organizing reasoning through introduction and elimination rules and the explicit discharge of assumptions. The display is not an algebraic fraction and should not be read as such. In the above rule, the first premise is the established source claim, the second says that the evidence establishes the relevant preservation result, and the third is the side condition that the claim lies in the class covered by that result.

The evidence may be a machine-checked proof. It may also include qualified tool evidence, timing analysis, test results, calibration data, configuration records, inspection, or operational evidence, depending on the transformation.

The proof at $M_0$ is not repeated at every stage. Instead, what must be repeated is the justification for transfer.

Four Outcomes Are Possible

When a formal claim reaches a more concrete representation or a realized system, four important different outcomes are possible. The claim(s) may be

Preserved
- The downstream claim retains the meaning and strength required by the architectural obligation, and the evidence establishes the relevant preservation relation. If the abstract property states that every detected hazard is followed by a safe response within 100 milliseconds, the realized system is shown to satisfy the corresponding physical and temporal claim under the stated fault and environmental assumptions and the claim has survived.
Weakened
- Some valid downstream claim remains, but it is weaker than the claim originally proved. Perhaps the software is shown to eventually issue a safe-state command, but no end-to-end 100-millisecond bound has been preserved. Or perhaps the bound holds only for a smaller fault set, a narrower temperature range, or a more restrictive workload. The original proof has not disappeared. It still supports the weaker claim. But the architectural obligation may remain unsatisfied. Weakening is especially dangerous when identical terminology conceals the change. “Recovery,”“availability,” “isolation,” and “safe state” may remain in the documentation while their quantified meaning contracts.
Invalidated
- The downstream artifact or system contains an admissible behavior that contradicts the transported claim. A schedule permits the deadline to be missed. A compiler transformation does not preserve the relevant semantics. An actuator saturates. A race condition introduces an execution absent from the verified model. Here the claim is false in the downstream representation or realization.
Inapplicable
- The conditions required to attach the formal claim to the downstream system have not been established. Perhaps the proof assumes reliable hazard detection, but no adequate relation has been shown between the formal event $H$ and the actual sensor chain. Perhaps the deployed processor, compiler version, configuration, or workload lies outside the verified basis. Perhaps the operating organization can change a parameter treated as fixed in the model. In these cases we are not yet entitled to say that the realized claim is false. We are also not entitled to say that it is true. The bridge needed to apply the proof is missing. This distinction matters. Invalidity calls for correction of a demonstrated violation. Inapplicability calls for recovery of the missing relation, assumption evidence, or boundary argument. Treating both as ordinary “verification failures” loses useful diagnostic information.

Safety, Liveness, Time, and Possibility Do Not Travel Identically

Different claims create different preservation burdens.

Suppose a concrete behavior relation establishes, after appropriate hiding or state mapping,

$\rho(\text{Beh}(C)) \subseteq \text{Beh}(A)$

If every relevant abstract behavior satisfies a trace property and the mapping preserves the property’s observations and semantics, this inclusion can be a powerful preservation result.

But several qualifications matter.

Safety

A safety property excludes bad behavior. If the concrete system introduces no mapped behavior outside the abstract specification, an abstract safety result often transfers naturally. That is one reason invariants and simulation relations are so useful in refinement proofs. Yet even here, the observables matter. A model can preserve the invariant

$\square{} \left( \text{commanded\_safe} \right)$

after a hazard while failing to preserve

$\square{} (\mbox{physical state} \in S_{\text{\tiny safe}})$

The first is a software-state claim. The second crosses an actuator and a physical plant.

Liveness and progress

Liveness properties require progress, i.e., under stated operating assumptions, a required event, response, or state transition must eventually occur. They exclude executions that remain indefinitely within allowed states such as through deadlock, starvation, or unintended divergence and without producing the outcome the architecture requires. Their preservation commonly depends on progress, fairness, non-divergence, or well-foundedness conditions that are not needed for a purely state-invariant argument.

A concrete implementation may take infinitely many internal steps while the abstract state appears merely to stutter. If the refinement argument permits that divergence, the concrete system may satisfy a safety simulation while failing to make the progress required by the architectural claim.

In a safety-critical system, the relevant liveness obligation may require continued delivery of a safety-critical service while its operating assumptions hold, or transition to a defined safe state when they no longer hold.

Alpern and Schneider formalized the general distinction between safety and liveness [AS85]. The important systems-engineering consequence is that a refinement proof adequate for invariance must not automatically be treated as adequate for progress.

Time

An untimed refinement cannot manufacture a quantitative deadline. If the architectural property is

$\square{}(H \Rightarrow \Diamond_{\leq \Delta} S)$

then detection latency, scheduling, computation time, communication delay, clock behavior, and actuator response all participate in the claim. Simulation techniques for timing-based systems exist precisely because time cannot always be erased and then recovered later [LV96].

Possibility and option preservation

Refinement commonly reduces nondeterminism by choosing among behaviors allowed by the abstract model. This is often desirable. But a claim that some future remains possible is not the same as a claim that all realized behaviors remain permitted.

Suppose the abstract architecture intentionally leaves two recovery mechanisms available

$\Diamond R_1 \vee \Diamond R_2$

A concrete implementation may select only $R_1$ . It can remain a perfectly valid behavioral refinement while eliminating $R_2$ as a future option. If the architectural obligation concerned functional correctness, nothing may be wrong. If it concerned recoverability, diversity, authority separation, or resilience under a later fault, an important claim may have been lost.

Refinement can therefore preserve permitted behavior while contracting the architectural future. This is not a contradiction. Instead, it’s another demonstration that preservation is claim-relative.

A Timed Hazard-Response Example

Consider an abstract controller with the property

$\varphi_A = \square (H_{\text{\tiny detected}} \Rightarrow \Diamond_{\leq 100\text{\tiny ms}} S_{\text{\tiny entered}})$

The model represents hazard detection as an event and entry into a safe state as a transition. A model checker establishes $M_A \models \varphi_A$ and the result is strong. That result is also about $M_A$ or the model.

Now refine the controller into tasks running on a processor. The transition is implemented through

$\text{sensor response} \to \text{sample acquisition} \to \text{hazard classification} \to \text{task release} \to \text{task execution} \to \text{network message} \to \text{actuator command} \to \text{plant response}$

An end-to-end bounded response now has the form

$T_{\text{\tiny response}} = T_{\text{\tiny sense}} + T_{\text{\tiny sample}} + T_{\text{\tiny classify}} + T_{\text{\tiny schedule}} + T_{\text{\tiny compute}} + T_{\text{\tiny network}} + T_{\text{\tiny actuate}}$

To preserve the original claim, we need more than a proof that the software eventually emits the right command. We need evidence that

$T_{\text{\tiny response}} \leq 100 \text{ms}$

under the admissible workloads, faults, clock tolerances, network conditions, and physical operating range.

We also need referential adequacy

Does $H_{\text{\tiny detected}}$ correspond to the hazard of concern, including sensor placement, thresholds, sampling, and fault behavior?
Does $S_{\text{\tiny entered}}$ mean that a software variable changed, that a command was transmitted, that an actuator moved, or that the physical system actually entered the required state?
Is the 100 ms interval measured from physical hazard onset, sensor detection, task release, or software classification?

Each interpretation yields a different claim. The abstract proof may survive as a software ordering property while being weakened as an end-to-end timing property. It may be invalidated by an admissible schedule. It may be inapplicable because the sensor-to-event relation was never established. Or it may be preserved through a combination of timed refinement, schedule analysis, worst case execution-time evidence, verified communication behavior, hardware qualification, calibration, and system-level verification.

The formal proof is still doing real work. It prevents one large class of controller behaviors from being possible. But it participates in a larger assurance argument whose other evidence is attached to the transformations the formal model did not contain.

Added Detail Creates New Obligations

Refinement is sometimes described as the progressive introduction of design detail. However, detail is not semantically free.

Introducing concurrency creates interference and scheduling obligations
Introducing a network creates delay, loss, ordering, identity, and authority obligations
Introducing numerical representations creates range, precision, overflow, and rounding obligations
Introducing hardware creates timing, failure-mode, electromagnetic, temperature, power, and manufacturing obligations
Introducing human operation creates training, authority, workload, procedure, and interpretation obligations

A refinement step must therefore do two things. It must

Preserve the inherited claims and assumptions for which it is responsible
Expose and discharge the new obligations created by the detail it introduces

Let $\Omega_i$ denote the active obligation set at stage $i$ . A useful schematic representation of the next stage obligation is

$\Omega_{i+1} = \text{Carry}_{\rho_{i}} \cup \text{New}_{i+1} \\ \text{Discharged}_{i+1}$

The expression is not intended as literal set subtraction for every engineering method. The purpose is to show how the obligations balance. Some obligations are carried forward. Some are transformed. Some are discharged. Some are weakened by an explicit decision. And some new obligations appear because a previously abstract choice has become a concrete mechanism.

This remainder is a realization residual, i.e., the set of inherited or newly created obligations that remain to be justified after a refinement step. From this we obtain a useful principle

Realization-Residual Principle

A valid refinement can preserve an abstract claim while creating additional architectural obligations. Those obligations are not defects in the proof. They are consequences of the new causal detail introduced by realization.

This is why passing every formal proof obligation in a design model need not mean that the realization is complete. The proof obligations generated by the formal method are a disciplined subset of the architectural obligations generated through refinement into something concrete.

Compilation Is Part of the Assurance Argument

Software makes the transformation chain especially visible.

A property proved about source code does not automatically become a property of machine code merely because a compiler produced the executable. The compiler and the act of compilation creates a semantic transformation from source code to object code or binary code.

CompCert demonstrates what it means to treat that transformation as an explicit preservation problem. Its central result is a machine-checked proof of semantic preservation across compilation from a substantial C-like source language to assembly [Ler09].

The significance for architecture is not that every system must use CompCert. The significance is that the source-to-executable arrow contains a claim that can be stated, proved, bounded, and audited.

Even a verified compiler retains a trusted computing base and semantic scope. The analysis by Monniaux and Boulmé is valuable precisely because it examines the places where errors or assumptions outside the central compiler proof can still matter [MB22].

Where verifying an entire translator is impractical, however, translation validation offers another pattern in that we can validate the result of each individual translation rather than proving the translator correct for all possible inputs [PSS98].

These approaches illustrate a broader point

A transformation tool is not merely a production convenience. When a proved claim must cross the transformation, the tool and its output become part of the preservation argument.

The same reasoning applies to model generators, code generators, linkers, configuration compilers, deployment scripts, theorem-prover kernels, and data conversion pipelines. Tool qualification, verified transformation, translation validation, independent checking, and output conformance testing are different responses to the same architectural question

What evidence justifies carrying this claim across this transformation?

How Far Down Can the Proof Go?

The seL4 verification program [KAE+14] provides a particularly instructive positive example because its assurance argument was deliberately extended through several representation levels.

The work includes functional correctness from an abstract specification to a C implementation, additional security properties, a connection to binary code for supported configurations, and analysis of other low-level concerns [KAE+14].

The lesson is not that the proof contains the entire deployed world. The seL4 work is explicit about assumptions concerning hardware, tools, and the scope of verified configurations. That explicitness is a strength because it reveals an important asymmetry.

Extending proof downward can eliminate or reduce some realization gaps. It does not erase the need to identify the remaining boundary.

A verified kernel does not prove every user application correct
A verified compiler does not prove the source program satisfies its requirements
A binary-level correspondence does not prove the processor is free of every physical fault
A verified software stack does not establish that sensors refer correctly to the phenomena assumed by the model

Formal assurance can extend remarkably far. But far is not the same as unbounded.

The architectural task is to know exactly where the proof reaches, what claim arrives there, and what evidence continues beyond it.

Situated Operation Is Another Refinement Boundary

Engineering accounts often treat deployment as the end of refinement. However, for many claims it is another beginning.

The deployed system enters an environment containing actual workloads, operators, maintainers, supply chains, policies, adversaries, weather, electromagnetic conditions, institutional authority, and changing mission purposes.

Some of these were represented as variables or assumptions
Some were excluded
Some did not exist when the proof was constructed

Leveson’s systems-theoretic account of safety is relevant because it treats safety as a control problem spanning interacting technical, human, organizational, and regulatory structures instead of a property reducible to component reliability alone [Lev11]. An operational change can therefore defeat a proved claim without changing the proved artifact.

A maintenance procedure changes a calibration constant
A governance authority grants an exception
A network is connected to a new domain
A workload moves beyond the analyzed range
A supplier substitutes a component
An operator develops a workaround that bypasses an interlock

The original proof may remain valid in its formal world. What fails, though, is the applicability relation between that world and the situated operation of the system.

This yields another principle

Operational-Applicability Principle

A proof survives situated use only while the realized system, environment, authority structure, and operational practices continue to satisfy the assumptions and interpretation relations on which claim transfer depends.

This makes monitoring and change control epistemically important.

Monitoring is not merely observing whether the system remains “green.” It should also test whether the conditions that make earlier evidence applicable remain true.

Verification and Validation Remain Distinct

Formal refinement is often exceptionally strong verification evidence. It can establish that a concrete artifact conforms to an abstract specification under a precise relation.

Validation asks a different question

Does the specification, and the system realized from it, address the right stakeholder purpose in the encountered environment?

A perfect refinement chain can preserve the wrong claim.

If $M_0 \models \varphi_0$ but $\varphi_0$ was not an adequate formalization of the architectural obligation, then flawless downstream preservation delivers the mistake with high fidelity.

This is the implementation form of the Nested Fidelity Principle introduced in Part 3.

Fidelity between adjacent representations does not establish fidelity to the underlying system or purpose. Each transformation carries its own claim-relative preservation obligation.

The full reasoning has two directions.

Downward, we ask whether the claim survives formalization, refinement, realization, and deployment. Upward, we ask whether evidence from the encountered system supports the interpretations and assumptions used in the formal account.

Proof pushes consequences downward. Validation and observation push evidence upward. Strong assurance requires the two to meet.

Formal Proof Is Evidence Within Governance

Once a formal claim enters a regulated or governed lifecycle, another mistake becomes possible: treating the proof as though it eliminates the need for an assurance argument.

It does not.

An assurance argument identifies the claim, evidence, inference, scope, assumptions, and residual uncertainty by which a decision authority is asked to accept risk.

Formal proof can be among the strongest evidence in that structure. But governance must still determine

Which claim is relevant to the decision
What level of assurance is required
Which assumptions are acceptable
What evidence is independent
What remains outside the formal boundary
Who has authority to accept the residual
What changes require reconsideration

DO-333 is instructive in this regard because it integrates formal methods into the objectives and lifecycle framework of DO-178C and DO-278A rather than declaring formal proof as a universal substitute for lifecycle assurance [RTC11]. The associated NASA case studies focus on the evidence formal methods can produce for particular certification objectives, not on an undifferentiated claim that the software is simply “proved correct” [CM14].

This is the proper relation between proof and governance.

Proof can make some conclusions nonnegotiable within the formal system. Governance decides whether those conclusions, their assumptions, and the remaining evidence justify commitment in the engineering world.

Formal methods do not determine the organizationally correct decision order or replace judgment about acceptable risk. They can, however, expose dependencies among decisions (cf., the previous post on “Decisions Do Not Commute”). If a downstream commitment requires preservation of a claim whose abstraction relation, timing basis, or operational assumptions remain unresolved, the formal structure can show that the commitment is premature.

In that sense, formal methods can function as decision-ordering instruments without becoming decision authorities.

The Claim-Preservation Record

If a proof is expected to survive realization, the engineering record should carry more than the theorem and final artifact.

For each important claim, a claim-preservation record should identify at least

The architectural claim and its intended interpretation
The formal proposition proved and the formal environment in which it was established
The claim class involved, such as safety, liveness, timing, probabilistic, resource, epistemic, deontic, or hyper-property
The sequence of representations and realized artifacts through which the claim must move
The abstraction, refinement, semantic-translation, or conformance relation used at each transition
The evidence establishing each relation
The assumptions consumed, transformed, introduced, or discharged at each stage
Any weakening of the claim and the authority that accepted it
The realization residual introduced by added detail
The versions of tools, models, source, generated artifacts, hardware, and configuration to which the evidence applies
The operational observations that support continued applicability
The change conditions that require re-verification, re-validation, or renewed architectural review

This is not merely traceability. Traceability may tell us that requirement $R$ is linked to model element $M$ , test $T$ , and code unit $C$ . The preservation record tells us why the claim embodied in $R$ is believed to retain its meaning through $M$ , $C$ , $T$ , and the deployed system.

That difference is architectural decision memory. Without it, later engineers inherit a proof artifact and a chain of links but not the theory that explains what the links preserve and why.

When Can We Say That the Proof Survived?

Let the final encountered realization be $\mathcal{R}$ , and let $\widehat{\varphi}_n$ be the operational interpretation of the original formal claim.

A defensible conclusion has the schematic form

$M_0 \models \varphi_0 \quad \wedge \quad \bigwedge\limits_{t=0}^{n-1} \text{Preserve}_i(\rho_i, \tau_i, \mathcal{C}_i, E_i) \quad \wedge \quad \text{Applicable}(\mathcal{R}, A_n, B_n) \Rightarrow \mathcal{R} \Vdash \widehat{\varphi_n}$

where

$\rho_i$ relates adjacent representations or artifacts
$\tau_i$ translates the claim between their vocabularies and semantics
$\mathcal{C}_i$ identifies the claim class preserved by the relation
$E_i$ is the evidence that the preservation obligation holds
$A_n$ is the active assumption set at realization
$B_n$ is the operationally relevant architectural boundary

The symbol $\Vdash$ is used deliberately. The final relation may combine formal satisfaction with empirical, causal, procedural, and governance evidence. The system as built, deployed, and encountered in use is not necessarily another mathematical structure available to the same proof calculus.

This conclusion is conditional. All serious engineering conclusions are.

The strength of it lies in making the conditions visible.

What Formal Methods Finally Give Architecture

The four parts of this series have followed one argument.

Logic is not external to the formal architecture. It shapes what can be expressed, distinguished, and proved.
Different claims and layers may require different logical environments, with explicit translations where meaning crosses among them.
A formal proof establishes a result inside a representation, under a logic, semantics, assumptions, and boundary. It does not by itself establish the adequacy of that representation or its identity with the encountered system.
A proved claim reaches operation only through a chain of preservation and applicability arguments.

None of this is intended to nor does diminish formal methods. It explains their architectural power.

Formal methods make claims precise enough to contest
They expose assumptions that informal confidence leaves hidden
They distinguish reachable behavior from imagined behavior
They reveal counterexamples before realization makes them expensive
They make refinement obligations explicit
They allow some transformations to be proved rather than merely trusted
They can preserve architectural knowledge across development stages when the proof, claim, semantics, assumptions, and preservation relations travel together

The proof survives implementation when the architecture carries that proof: not as an isolated certificate. But as a living structure of claims, relations, evidence, assumptions, obligations, and conditions for reconsideration.

That is the proper place of formal methods in systems engineering.

References

[Abr10] Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge, 2010.

[AL91] Martín Abadi and Leslie Lamport. The Existence of Refinement Mappings. Proceedings of the 3rd Annual Symposium on Logic in Computer Science. July, 1988.

[AS85] Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 1985.

[CM14] Darren D. Cofer and Steven P. Miller. Formal methods case studies for DO-333. Technical Report NASA/CR-2014-218244, National Aeronautics and Space Administration, Washington, DC, 2014.

[CS10] Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157–1210, 2010.

[dRE98] Willem-Paul de Roever and Kai Engelhardt. Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge University Press, Cambridge, 1998.

[Gen35] Gerhard Gentzen. Untersuchungen über das logische Schließen (I). Mathematical Zeitschrift, 39:176-210, 1935.

[Gen69] Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, volume 55 of Studies in Logic and the Foundations of Mathematics, pp. 68-131. North-Holland, Amsterdam, 1969. English translation of Untersuchungen über das logische Schließen, I-II.

[ISO22] ISO/IEC/IEEE. ISO/IEC/IEEE 42010:2022, Software, Systems and Enterprise— Architecture Description. International standard, International Organization for Standardization, 2022.

[ISO23] ISO/IEC/IEEE. ISO/IEC/IEEE 15288:2023, Systems and Software Engineering—System Life Cycle Processes. International standard, International Organization for Standardization, 2023.

[KAE+14] Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):1–70, 2014.

[Ler09] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009.

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

[LV95] Nancy A. Lynch and Frits W. Vaandrager. Forward and Backward Simulations, Part I: Untimed systems. Information and Computation, 121(2):214–233, 1995.

[LV96] Nancy A. Lynch and Frits W. Vaandrager. Forward and Backward Simulations, Part II: Timing-based systems. Information and Computation, 128(1):1–25, 1996.

[MB22] David Monniaux and Sylvain Boulmé. The Trusted Computing Base of the CompCert Verified Compiler. In Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, volume 13240 of Lecture Notes in Computer Science, pages 204–233. Springer, 2022.

[Pra65] Dag Prawitz. Natural Deduction: A Proof-Theoretical Study. Number 3 in Acta Universitatis Stockholmiensis: Stockholm Studies in Philosophy. Almqvist & Wiksell, Stockholm, 1965.

[PSS98] Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Bernhard Steffen, editor, Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 151–166. Springer, 1998.

[RTC11] RTCA. DO-333: Formal Methods Supplement to DO-178C and DO-278A. Technical report, RTCA, Inc., Washington, DC, 2011.