The formal language HLL (High Level Language) has emerged in recent years as a quite popular language for formal verification of safety-critical systems, especially in the railway signaling domain. This year marks the 10th anniversary of its conception.
The history of HLL
The language has its roots in the proof engine technologies developed by Prover in the 1980s (Stålmarck’s method), 1990s (temporal induction) and early 2000s (higher level theories) and its development was prompted by a need for trusted (or certifiable) formal verification.
HLL is a declarative language with a broad panel of types and operators and is suitable for modelling discrete-time sequential behaviors and expressing properties of these behaviors.
Or to put it differently: if you have a reactive system (such as an interlocking or a CBTC subsystem) with some inputs, outputs and internal state (memory), and you want to formally prove that some present or future conditions on the outputs shall follow from some past or present conditions on the inputs, then HLL may be the right language for you. The language, with its associated tools, can be used for applications such as invariant checking, sequential equivalence checking, test case generation or static code analysis (detection of runtime errors such as overflows or divisions by zero).
Version 1.0 of HLL was released in 2008 and the language is being continually developed. The latest version includes, in addition to the basic core of Boolean logic and integer arithmetic, features such as enums, arrays, tuples, structs, recursive functions, quantifiers, polymorphism, namespaces and blocks. The imperative dialect of HLL also supports statements such as assignments, if-then-else, loops and procedures.
The HLL formal language success
The success of HLL can possibly be attributed to its ease of use (flexible and intuitive) coupled with the support by formal verification tools that both scale up in practice for a wide variety of systems, and provide certifiable results based on diversification and proof logging/checking.
Find out more about HLL here.
You can also check out our HLL Forum – The community for those who use HLL
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
Do you have experience in leading strategic and complex customer projects? Are you looking for an opportunity to leverage your experience throughout our company? Then this role might be right for you! We are now recruiting to a new position as a Commercial Project Management (PM) Lead.
Prover uses formal methods to make railway signaling provably safe. Our solutions build safe, reliable, and cost-efficient systems that move and protect millions of passengers every day. Through our Open Signaling Initiative, we're reshaping how the industry builds and maintains signaling systems across Europe and beyond. Now we're looking for someone to join us and bring AI, LLMs, and agentic workflows into the heart of how we work and what we build.
Meet Prover at RailTech Europe in Utrecht, March 4–5. Visit Booth 2.509 and join our workshop on migration of signaling systems to PLC-based SIL 4 solutions.
