Welcome to Lemma 1!
This is the home page for Lemma 1 Ltd.
Lemma 1 provides consultancy in software engineering. We specialise
in tools and methods for applying formal, mathematical, methods for specifying,
designing and verifying critical software systems. We can also undertake
software development in a range of programming languages and operating
If you would like to get in touch, please contact Rob Arthan by e-mail
- ProofPower — a suite of tools
for specification and proof in HOL and Z; also the Compliance Tool for
specifying and verifying Ada programs.
The HOL and Z tools are free open source software.
You can obtain ProofPower from the
- Z STANDARDS PAGE
— some contributions to the ISO standardisation of the Z specification
- PAPERS — some papers on formal methods.
- ClawZ — reports from a project
that researched the possibility of using Z to model Simulink diagrams.
The successor to the prototype tool developed in this project is now
being actively exploited by
- SCRAPBOOK — odds and ends.
Created by Rob Arthan
Last updated: $Date: 2014/01/23 16:40:34 $