Who actually uses this

When someone in the equipment industry hears about a new method, the first thing they want to know is not how well it works.

“So who’s using it?”

That question is not asked out of suspicion. A machine runs for more than ten years. If the production line you shipped it to stops, the responsibility comes back to you. You cannot put something with no track record into a customer’s machine — that is not caution, it is an ordinary premise of the business.

So that question gets answered first. How well it works comes after.

AWS has been using it since 2011

Amazon Web Services has used a formal method called TLA+ on real production systems since 2011. This is not an experiment in a research division. They use it on the design of services that are running, and internally the executive level has actively pushed it. The engineers who did the work wrote it up themselves in a paper, “Use of Formal Methods at Amazon Web Services”, published on the site of Lamport, the author of TLA+.

Why they go that far is easy for equipment people to follow. The whole of the AWS business rides on distributed systems behaving correctly. And the expensive errors in a distributed system are not mistyped code. They are rare orderings that appear only when several things move at once.

Things moving at once. Orderings that surface only rarely. Events that cannot be reproduced by testing — the same kind of error that equipment engineers call “it stops sometimes”.

Airbus is investigating whether it can replace unit testing

Airbus is examining whether formal methods can replace unit testing.

The weight of that sentence is worth stopping on. What they are investigating is not “can it be used as an aid to testing”. It is “can it stand in place of testing”. Unit testing on an aircraft is not work you do if you feel like it; it is work you must do for certification. Whether that can be substituted by other means is being treated as a serious question.

To be clear, this is at the investigation stage; it is not a story about a completed replacement. But it has come far enough to be capable of being investigated at all. Not many techniques get named as a candidate substitute for a mandated verification activity.

CERN and GSI put PLC verification out as a “service”

For the equipment industry, I think this is the closest precedent.

CERN and GSI have published work under the name “Formal Verification of PLCs as a Service”. There are two places worth reading closely.

The first is PLC. Not a web server, not an aircraft’s control computer. The same industrial control hardware that runs factory equipment. If formal methods only held up inside the cloud or inside aerospace, this would have nothing to do with us. But this is aimed at industrial control itself.

The second is as a Service. That is, it does not assume a formal methods specialist sitting on the side of the team writing the PLC code. The specialist is outside, and only the verification is supplied from outside. The people building the machine carry on building the machine.

Hiring and growing an in-house formal methods specialist is not realistic for a mid-sized equipment maker. Receiving verification from outside changes the conversation. It is the published case that comes closest to a form a mid-sized equipment maker could actually buy. It is also the form we are trying to build.

What the three cases have in common

Cloud infrastructure, aircraft, accelerator control. Lined up, they look as though they have nothing to do with each other. And nothing to do with the equipment industry either.

There is one thing in common. All of them are systems in which several things move at once, and in all of them the expensive errors sit on the side that testing cannot reproduce.

So they paid not in the direction of thickening the testing, but in the direction of examining the design itself. Because they admitted, early on, that a human cannot count the combinations of orderings.

Automation equipment is a member of this family. There are axes, there is transfer, there is host control, there are interlocks, and they all move at once. It stops only when they mesh in a rare order. The structure is the same. It just has not been described that way yet.

Let me put this honestly — it is not widespread

Read this far and it might sound like a technique on its way to becoming an industry standard. It is not.

Industrial adoption of formal methods is still limited and niche. That is not an assessment from opponents. AWS says so themselves. The party that has used it for more than ten years is the one saying it has not spread.

So does it fail to spread because it does not work? In a survey of 130 experts, 71.5% named “insufficient engineer education” as the biggest barrier to adoption. The top answer was not “it is doubtful whether the technique is effective”. It was there is nobody who can use it.

In other words, the place where things are stuck is not the technology side. It is the people side.

The technology is proven. The adoption is not.

This is the actual state of the world. Organisations that were not permitted to get it wrong have been using it for more than ten years. Everyone else has not touched it. It is neither “everybody is doing it” nor “this is the future”. The fact that it is neither is the answer we have in hand right now.

So “it is not widespread yet, so it is risky” and “it is already the industry standard, so hurry” are both wrong readings of the situation. The correct reading is this — that it works is already known. What remains is only whether there is a road by which you can come to use it.

And what the CERN and GSI case shows is that this road is not limited to “grow a specialist in house”.

What to read next

It is not only forward-leaning companies that ask for formal methods. The safety standards themselves require them, conditionally. That situation is covered in Why safety standards ask for formal methods.

And why equipment software cannot lean wholly on testing in the first place — that structure is in Why equipment software cannot run the right-hand side of the V-model.