What comes after "design with models"

Put a machine from ten years ago next to a machine built today. The difference is not size. It is the number of people involved.

Mechanical, electrical, control, software, safety. Each has an owner, and each owner writes something that is correct within their own scope. Problems still appear at commissioning. And when you go back and reread each owner’s documents, the problem is not in any of them. A behaviour written into nobody’s design appears the moment the machine is assembled.

The machine no longer fits inside one person’s head. Somewhere along the way, the specification and the physical machine quietly drift apart. There is probably no equipment engineer who does not recognise this.

And it did not only happen to the equipment industry.

The world has already begun designing with models

Automotive, aerospace and medical devices all hit the same wall. The answer that emerged was to hold the design as a model rather than as documents. Model-Based Systems Engineering, Model-Based Design. There are several names for it, but the activity is the same: requirements, states and interfaces are written as structures a machine can process, not as prose for a human to read.

Drawing block diagrams in Simulink, writing state machines in SysML, linking requirements to modules in a design management tool — all of it belongs to this movement. Your company may already be doing one of them — just not calling it that.

This is not somebody’s bright idea; it is a market in motion. Third-party research estimates the MBSE market at roughly 7.4 billion dollars in 2024, growing to roughly 22.7 billion dollars by 2033 — a compound annual growth rate of about 13%. Those are not the numbers of “a promising new idea”. They are the numbers of a migration that has already started.

In other words, a great many organisations already have a foot on this ladder.

Modelling only takes you as far as building the model

Let us list what a modelling tool actually does for you.

• It gives you somewhere to write the model
• It shows the model as a diagram
• It checks that the model is well-formed (dangling references, type mismatches)
• It generates code from the model

The last one is powerful. The step in which a human transcribes by hand disappears, and with it an entire category of error — the transcription mistake — vanishes.

So ask this. Is that model correct?

No tool answers that question. Some appear to, but what they are looking at is whether the model is well-formed as a model — not whether running the machine according to that model is safe.

Code generates perfectly from an incorrect model too. There is not a single error in the generated code — in the sense that it does exactly what was written. The error is on the model’s side, and no amount of reading the code will bring it out. This is an error that a code review will never find.

Building a model and proving that the model is correct are two different jobs.

Different jobs need different tools.

Formal methods fill the gap

Laid out as a single ladder, it comes to this.

Machines grew complex; design stopped fitting inside heads and paper
  → so the world moved to designing with models (MBSE / MBD)
  → but nobody proves whether those models are actually correct
  → verification by formal methods fills that gap

The name “formal methods” may be unfamiliar. What it does is simple. You put the states and transitions written in the design into a form that can be handled mathematically, and let a machine exhaust the combinations of states that can occur. All of them — including the orderings nobody thought of. If there is even one path along which a safety condition breaks, it finds that path and hands it back.

The important point is that this is a layer that sits one rung higher on the ladder. It does not stand alongside the others and compete with them.

Let us dispose of the obvious worry first. You do not have to throw away Simulink. The PLC toolchain stays, the in-house design management stays, the procedures in the quality manual stay. You build models exactly as you do now. One step is inserted before code generation, in which you ask that model whether a sequence exists in which both axes enter the hazardous zone at the same time. That is all.

The entry point is a design artefact you already have — that is the crux of it. The detailed design already states what states the machine has, in what order it moves, and under what conditions the interlocks engage. The raw material is there.

The better code generation gets, the more the design becomes the bottleneck

Hand over a detailed design and get code back: that is becoming real. How far the equipment industry will accept it is a separate argument, but as a technology, it is here.

This does not remove the problem. It moves it.

If the design is wrong, the AI will implement that wrong design accurately. Faster than by hand, more accurately, and in greater volume. And the error will be nowhere in the code — because it is in the design.

The better code generation gets, the more the design becomes the bottleneck. Load accumulates at the least automated part of the process. That is all it is. But how heavy that “all” turns out to be depends entirely on whether you have a way to check the design.

So why isn’t everyone doing this?

Let us be honest here. This ladder is not easy to climb.

MBSE itself is not spreading smoothly. A 2024 INCOSE survey names three barriers to adoption — perceived complexity, compatibility with existing practice, and the learning curve.

As you can see, none of them is technical. “It looks hard.” “It doesn’t mesh with how we work now.” “It takes time to learn.” Formal methods run into exactly the same three walls. If anything, harder than MBSE does. The moment mathematical notation appears, most organisations stop. That is not laziness; it is a reasonable judgement.

If that is so, then what is needed to make this rung actually climbable is not more theory. It is that what the designer already writes becomes the entry point, unchanged, and that the result comes back in the language of the field. Until that is solved, proofs of correctness stay inside papers.

DatumProof exists to make this rung something an equipment engineer can step onto using their ordinary design artefacts, just as they are.

What to read next

“Check the design” — but how is that different from testing? Until that lands, nothing else does. It is covered in What is the difference between testing and formal methods?.

And whether methods like this are actually in use. The answer is that they are, and not far from the equipment industry at that. Who actually uses this introduces them.