InduByte logo

Formal verification of PLC software

Programmable Logic Controllers (PLCs) control critical machinery in vital industries, such as oil & gas, petrochemicals, energy, water & wastewater, transportation & infrastructure, and manufacturing.

The consequences of defects in PLC software can be severe: endangering lives, harming the environment, or disrupting essential services.

InduByte offers advanced tools and services to detect PLC software defects with mathematical rigour — far beyond the capabilities of traditional testing methods.

Why formal verification?

Traditional testing explores only a limited number of scenarios. As a result, software defects can slip through unnoticed, until they cause critical failures in the real world.

Program testing can be used to show the presence of bugs, but never to show their absence!

This limitation has been recognised since the early days of computing. Yet many companies still rely solely on testing to validate critical PLC software.

Formal verification goes further. It uses mathematical techniques to exhaustively check that a PLC program behaves correctly in all possible situations — including edge cases no human tester could foresee. This allows us to prove that software meets its requirements under any circumstance.

A typical verification flow: from PLC program and requirement to model checking and results.

Our Tools & Services

Our platform offers a practical way to apply formal verification to real-world PLC software. Engineers provide the PLC program and a formally expressed requirement. We then use model checking to verify whether the program satisfies this requirement — exhaustively and with mathematical precision.

While the tooling is designed for engineers to use independently, we offer a range of services to help you integrate and scale it effectively:

With a strong background in industrial automation, we speak your language. This enables us to work closely with your team, making verification practical, fast, and insightful.