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 environments.

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 download page.
Z STANDARDS PAGE — some contributions to the ISO standardisation of the Z specification language.
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 D-RisQ Ltd..
SCRAPBOOK — odds and ends.

If you would like to get in touch, please contact Rob Arthan by e-mail at [rda at lemma-one dot com]

Created by Rob Arthan [rda at lemma-one dot com]

Last updated: $Date: 2014/01/23 16:40:34 $