Formal Methods Wiki

Virtual Library
Software engineering
Formal methods

Formal Methods Companies

Please edit this page with information on formal methods companies. Alternatively, please contact Jonathan Bowen if you know of relevant online information not included here, would like to maintain information for a particular company, or have any corrections.

This document contains some pointers to companies with some interest in formal methods, most of which provide on-line access to information on the World Wide Web.

Abstract Hardware Limited, Uxbridge, Middlesex, UK.
Products including the LAMBDA system synthesis tool set and PolyML, a commercially supported version of Standard ML. Services include training courses and consultancy.
Now ceased operation.
AbsInt, Germany.
Advanced development tools for embedded systems, and tools for validation, verification and certification of safety-critical software.
Adelard, London, UK.
Consultancy in the areas of: development, verification and assessment; safety cases; standards and guidelines; training and technology transfer.
AeS Group , Sao Paulo, Brazil.
Consultancy in software and system development, safety case assessment and development. Railway system developer.
ATX Software, Portugal.
Coordination Development Environment (CDE) tool.
B-Core (UK) Limited, Oxford, UK.
B-Toolkit, based on the B-Tool.
Bell Labs, New Jersey, USA.
Part of Lucent Technologies.
Bell Labs Design Automation have produced the FormalCheck tool for verifying the functionality of ASIC and digital IC designs in Verilog or VHDL, based on the COSPAN model checker.
BT Laboratories, Martlesham, Ipswich, UK.
Formal [ Methods Group. Contact Elspeth Cusack on for further information. ]
Cap Gemini, Utrecht, The Netherlands. (Was Cap Volmac.)
VDM++ language and tools. Afrodite project. Contact Nico Plat on
Chrysalis Symbolic Design, Inc., North Billerica, MA, USA.
Produces software for creating and verifying electronic circuits and systems. Products include Symbolic Logic (tm) technology to help with formal verification.
ClearSy System Engineering, Aix-en-Provence & Paris, France.
Maintainer of Atelier B tool and consulting based on B-Method. Special consultant: J.-R. Abrial. (In French.)
Computational Logic Inc., Austin, Texas, USA.
Nqthm and Pc-Nqthm theorem proving tools. Hardware verification including the FM9001 microprocessor.
Ceased 1997.
Daimler-Benz Research, Berlin, Germany.
Local organizers and sponsors of ZUM'98, Berlin, September 1998.
Danish State Railways (DSB), Denmark.
Members of the ProCoS-WG Working Group. Contact Kirsten Mark Hansen on
Digilog, France.
Atelier B tool supporting the B-Method. Contact Francois Bustany on
DST (Deutsche System-Technik GmbH), Kiel, Germany.
Members of the ProCoS-WG Working Group.
Ceased trading in November 1996. All former employees now work for VST.
Escher Technologies, UK.
Consultancy including formal verification.
Escher C Verifier (eCv) tool for formal verification of MISRA-C programs.
Perfect Developer tool for formal specification, refinement and code generation.
Esterel Technologies, France.
Esterel Studio tool for verification and validation, based on the Esterel language.
Flowgate Consulting, Rosario, Argentina
Model-based testing for the Z notation with Fastest.
Formal Systems (Europe) Ltd., Oxford, UK.
CSP software including FDR2 model checker.
See also earlier FDR tool for CSP model checking. Contact
GEC Alsthom, Paris, France.
Users of the B-Tool.
Members of the ProCoS-WG Working Group.
Contact Babak Dehbonei or Fernando Mejia on fax: +33 (1) 40 10 65 00 (no email!).
Harlequin, Australia / UK / USA.
Consultancy including formal software engineering and reasoning systems.
Headway Software, Calgary, Canada.
Consultancy. Formal modelling using Z, VDM, UML, etc. Rose Formaliser Link (Z and UML).
IBM United Kingdom Laboratories, Hursley Park, UK.
See 1992 Queen's Award for work on CICS. See also IBM's Cleanroom Software Technology Center, Clear Lake, Texas USA.
Original developer of ProofPower, a tool based on HOL for proofs about Z specifications.
* IFAD, Odense, Denmark.
Products include VDMTools supporting VDM-SL and VDM++.
Consultancy, training and technology transfer of VDM.
VDM repository.
Members of the ProCoS-WG Working Group.
Industrilogik L4i AB now Prover Technology, Stockholm, Sweden.
Safety and quality using formal methods. Consultancy, R&D.
Inmos, Bristol, UK.
Now SGS-Thomson Microelectronics.
See 1990 Queen's Award for work on the T800 transputer.
See also PACT (Partnership in Advanced Computing Technologies), occam programming language and safemos project.
IST (Imperial Software Technology Ltd), Reading, UK. (Also Cambridge, London, and Palo Alto, USA.)
Software engineering company, including an Advanced Technology Group specializing in the application of formal methods for high-integrity and secure systems.
Products include Zola, an integrated editor, type-checker and prover for the Z notation.
Kestrel Institute, California, USA.
Undertakes research in applying formal methods and automated reasoning systems to software engineering.
K&M Technologies Limited, Dublin, Ireland.
Industrial exploitation of the Irish School of the VDM, etc.
Lemma 1 Ltd., Reading, UK.
Founded 1997.
Consultancy company run by Rob Arthan, previously at ICL.
Co-located with InterGlossa Ltd.
Experience of the ProofPower tool for Z proofs.
Lloyds Register, Croydon, UK.
Members of the B User Trials project.
Members of the ProCoS-WG Working Group.
Members of the REDO project.
Logica UK Limited.
Formal methods tools and services, including the Formaliser Z type-checker. Contact Susan Stepney on for further information.
Logikkonsult NP AB, Sweden.
See Prover Technology.
Mentor Graphics Corporation, Wilsonville, Oregon, USA.
Hardware system design and verification.
formal verification equivalency checker for multi-million gate ASIC and SoC (system-on-a-chip) verification.
Seamless hardware/software co-verification.
National Physical Laboratory (NPL), UK.
Market Prover from Prover Technology.
Members of the ProCoS-WG Working Group.
ORA Canada, Ottawa, Canada.
EVES and Z/EVES proof tools.
Philips GmbH Forschungslaboratorien, Aachen, Germany.
Members of the ProCoS-WG Working Group.
Praxis Critical Systems, Bath, UK.
Separated from Praxis in April 1997. Skills in formal specification, static analysis, safety engineering.
Products include SPARK language and tool support for program verification.
Contact Anthony Hall on for formal methods course information.
Contact Amanda Kingscote on to join the Z postal mailing list.
Members of the ProCoS-WG Working Group. Contact Trevor King on
Program Validation Limited, UK.
Now Praxis Critical Systems.
Members of the B User Trials project.
Prover Technology, Sweden.
See proof engine Prover iLock Verifier Module. Previously known as Logikkonsult NP.
Prover provides solutions for specification, coding, simulation and formal verification of control and signalling applications.
Reactive Systems, Inc., USA.
Model checking.
Research Access Inc., USA.
Specification and verification documents.
Rolls Royce & Associates, Derby, UK.
Use VDM.
RWT*Uuml;V Anlagentechnik, Germany.
Members of the ProCoS-WG Working Group.
Safet, Buenos Aires, Argentina.
Safe software technologies, including verification.
SoftwareIntegrity, Inc., USA.
SoftwareExcelaration methodology.
* SRI, Menlo Park, California, USA. Also, Cambridge, UK.
Formal methods information and PVS tool.
Telelogic AB, Malm, Sweden.
Products include SDT, a software engineering toolset based on SDL, and the ITEX test suite tool.
Terma A/S, denmark.
Provider and user of RAISE (Rigorous Approach to Industrial Software Engineering).
Temporal-Rover tool based on temporal logic.
Transitive Technologies, Manchester, UK & San Diego, USA.
Uses formal methods "light" for optizing dynamic binary translation technology.
Contact John Fitzgerald on for formal methods aspects.
Verified System International GmbH, Bremen, Germany.
FDR model-checker and RT-Tester tools. (Information in German.)
Verilog, USA.
See also France. Products include the ObjectGEODE toolset, based on the OMT, SDL and MSC standards notations, dedicated to analysis, design, verification and validation through simulation, code generation and testing of real-time and distributed applications.
Verplex Systems, Inc., USA.
Formal verification and logical equivalence checking products for ASIC and IC applications, including the Tuxedo-LECTM tool.
See Verify99 seminar information.
Vossloh System-Technik GmbH (VST), Germany
Daughter company of the Vossloh AG.
Active in traffic sector (mainly railway).
Former employees or DST now work for VST.
Contact Hans-Martin H&oumlrcher, Vossloh System-Technik GmbH Edisonstr. 3, 24147 Kiel (tel: +49-431-7109-539, fax: -502, email:
WetStone Technologies, Inc., USA.
Information security.
See formal methods questionnaire.
York Software Engineering Ltd (YSE), UK
See products, including CADiZ Z type-checker;
Subsidiary of CSE.

See also:

Last updated by Jonathan Bowen, 18 November 2011.
Further information for possible inclusion is welcome.