Prover Studio

An Integrated Development Environment for Formal Specifications

About Prover Studio

A key element of the Prover Trident process is the Generic Application that formalizes the signalling requirements for your rail control applications using the PiSPEC and LCF languages. Prover Studio is a development environment integrated with the Prover iLock tool that helps you manage, develop and maintain these formal specifications.


Based on Visual Studio Code, Prover Studio provides all the expected features such as syntax highlighting, auto-completion, reporting of syntax and semantic errors and shortcuts to find definitions and references. Prover Studio is used to edit and keep track of the PiSPEC and LCF source files when the Generic Applications are developed, at the same time as Prover iLock is used to test and validate the specifications on Specific Application configurations, supporting an agile and test-driven development process.