High-Level Language

The global community for HLL

The HLL Forum is the community for users, providers, and enthusiasts of HLL — a powerful, industrial-ready formal specification and verification language used to design and validate safety-critical systems.

Why join the HLL Forum?

By joining the community, you ensure that your voice is heard in the evolution of HLL and that you stay up to date with the latest developments, resources, and opportunities within the HLL ecosystem.

Support and free resources

Explore free and helpful resources from the tool providers below, as well as the free HLL specifications. Whether you’re new to HLL or advancing your skills, these materials support your learning and use of the language.

Free specifications

Manifesto

The founders and history of HLL language specification

The HLL language was created in 2005 to support the formal verification of safety-critical railway systems. In 2018, the HLL Forum was established to unify the language, guide its evolution, and ensure long-term availability and interoperability.

HLL tool providers in alphabetical order

Prover has been working with formal verification since the 90’s and developed HLL for RATP starting 2005.

Prover provides several tools for HLL, such as the free IDE/editor Prover Studio, model checker Prover PSL and the sign-off verification tool Prover Certifier that is CENELEC EN 50716/50128 compliant up to the highest integrity level SIL 4.

Prover HLL Tools

Since its inception in 2001, formal methods have been at the core of Systerel offer, starting with the B method, then Event-B, and since 2009 HLL. Systerel started its verification suite Systerel Smart Solver (S3) in 2013, continuously qualified at T2 level for SIL4 systems (EN 50128:2011).

Systerel has also developed other use cases based on HLL: Back-to-Back Testing, Balise Layout Assistant, etc

Systerel HLL Tools

HLL users in alphabetical order

RATP

The RATP Group business unit, RATP Infrastructures, dedicated to maintenance, engineering and project development for the Paris Region railway network, initiated the development of HLL in 2005, to meet its needs for formal verification of railway systems.

Since then, RATP Infrastructures has played a key role in advancing HLL, first through shared intellectual property with the tool providers, and since 2018 through the HLL Forum.

As an expert and long-standing user, RATP Infrastructures has successfully used HLL in many formal verification projects, ensuring the highest standards of safety and reliability across its railway systems.

SL

SL (Stockholm Public Transport) has been using HLL for formal verification of Roslagsbanan signaling systems (CENELEC SIL 4) since 2012. This is now being extended to more lines. The use of formal verification is a way for SL to increase safety and discover issues early, as well as finding deviations from established practices in the design of signaling systems.