The FME Industry Committee maintains a list of companies using formal methods tools in some of their development process. If your company is not on this list but you would like to have it appear on there, then send an email to industry@fmeurope.org.
| Company | Tool |
|---|---|
| Airbus | Astree static analyzer |
| Airbus | Compcert verified compiler |
| Altran | SPARK Ada toolset |
| AWS | Dafny |
| AWS | TLA+ |
| AWS | Z3 |
| AtkinsRéalis | MALPAS Software Static Analysis Toolset |
| BAES | SPARK Ada toolset |
| ClearSy | Atelier B (for railway control) |
| Callen Lenz | Kapture |
| Callen Lenz | ModelWorks |
| D-RisQ | FDR4 |
| D-RisQ | Z3 |
| D-RisQ | ProofPower |
| D-RisQ | Temporal logic predicates used to check consistency within Kapture for software requirements |
| D-RisQ | ModelWorks for verification of Simulink/Stateflow designs against high level software requirements |
| D-RisQ | CLawZ for verification of C code automatically generated from Simulink/Stateflow Used on various Robotics and Autonomous Systems |
| Galois | Software Analysis Workbench (used to verify Amazon Web Services s2n encryption library) |
| Honeywell | PVS |
| Honeywell | Kapture |
| Honeywell | Variety of SMT solvers |
| Infer static analyser | |
| Microsoft | SLAM |
| NASA | PVS |
| NASA | Spin |
| Rolls Royce Aeroengines | SCADE |
| Rolls Royce Aeroengines | SPARK Ada toolset |