We offer tools and services to help you produce high-integrity software for safety-critical applications. Using advanced automated reasoning, our tools deliver the benefits of formal verification using a fraction of the effort demanded by other tools.

Choose from Perfect Developer for top-down modelling of requirements and specifications with optional code generation, or Escher C Verifier (eCv) if you prefer to write your code by hand in MISRA C/C++.

By using our tools to prove the system correct before it is built, you avoid the need for debug/re-work/re-test cycles. When used within a mature software development process, Perfect Developer and eCv can reduce the need for unit testing, by facilitating Correct by Construction software development.

We also provide a range of services to help you develop verified software, to verify existing software, or to develop critical software components for you.

Defence software development to UK DefStan 00-55, DefStan 00-56 or MIL-882

Defence Standard 00-55 mandates the use of formal proof for software that is highly critical to system safety, while version 3 of 00-56 cites formal proof as one of the highest forms of safety evidence and deprecates reliance on process-based evidence alone.

Not only do Perfect Developer and eCv reduce the cost of developing critical software, by providing formal proofs, but they also provide much of the safety evidence needed to achieve certification. Perfect Developer is already being used to develop critical airborne software to 00-55 SIL 4.

Development to IEC-61508

Perfect Developer and eCv are well-suited to the development of software to IEC 61508 safety standards, especially at the higher Safety Integrity Levels. Formal methods are recommended for developing SIL 2 and SIL 3 software (see Table A-1 of IEC 61508-3) and highly recommended for SIL 4 software.

By generating proofs automatically, our tools makes the production of formally-verified software quick and economical.

Aerospace software development to DO-178B

The FAA and NASA created the Object Oriented Technology in Aviation (OOTiA) program to examine and document issues arising when DO-178B certification is required for software developed using object-oriented techniques. The program has produced a Handbook for Object Oriented Technology in Aviation, highlighting these issues and providing guidance.

Perfect Developer provides solutions to almost all issues documented in the Handbook. For example, by using the verified design-by-contract paradigm, Perfect Developer guarantees that formal subtyping is achieved (section 3.3.7 of the handbook). Type conversions (section 3.7.4) are formally proved safe and are never performed implicitly. Overloading (section 3.8) is rendered safe by the absence of implicit conversions and the formal verification of behaviour.

Please contact us for further details.