Gateaux is a tool supporting verification in the OTS/CafeOBJ method,
which can do the following currently:
- Generate (templates or skeleton) of proof scores from Gateaux scripts,
- Have the CafeOBJ system execute proof scores generated automatically, and
check if the results are what expected,
The source code (Prototype Version 0.1) written in C is given.