We are pleased to announce that Prover, RATP, and Systerel have, through the HLL Forum, jointly published a unified specification of HLL 4.0 — the High Level Language for formal verification of safety-critical systems.
HLL is a formal language designed for model checking of discrete-time systems. It enables engineers to mathematically verify that safety-critical software — such as interlockings, ETCS, and CBTC systems — meets its safety requirements in 100% of possible scenarios, a level of assurance that testing alone cannot achieve.
HLL was initiated by RATP in 2005 to enable formal verification of railway systems and was later developed further together with Prover and Systerel. It became the de facto standard for model checking in the rail and metro domain and has since been adopted by other infrastructure owners including SNCF, SL and Trafikverket, but also by leading signaling suppliers such as Hitachi and Alstom.
The newly published specification of HLL 4.0 is a significant milestone: it ensures that HLL will not fork into different dialects as tool providers develop the language. By committing to develop HLL together, we avoid lock-in, enable fair competition, and remove an obstacle for adoption. The specification is donated to the public domain through the HLL Forum association.
Organizations who use HLL are warmly invited to join the HLL Forum — an association dedicated to promoting HLL, guiding its evolution, and developing its roadmap together. The next HLL Forum meeting will be organized soon.
Learn more at hllforum.org.
Share this article
Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Generative AI has entered railway software engineering ahead of the standards governing it. A new CENELEC draft amendment to EN 50716 doesn't add requirements. It clarifies which existing rules apply when AI drafts specs, writes code, or generates test cases, and why those rules are harder to satisfy with generative models than teams might assume.
Prover, together with NEAT, Schneider Electric, and Pilz will demo real railway interoperability at InnoTrans: three vendor platforms, one interlocking design, live at Prover's booth.
EULYNX standardizes rail signaling interfaces, but not the assurance behind them. Here's how formal methods close that gap, with exhaustive proof, generated test suites, and verified wrappers.
