Take nothing on its looks; take
everything on evidence. There's no better rule.
(Jaggers) C. Dickens Great Expectations.
However, those assistants lack automation.
Automation is hard to achieve in that context: in particular providing the results of external decision procedures is not sufficient. The proof assistant will refuse to handle a property if it does not come with a proof. That proof must be checked mechanically by the verification kernel. Hence, one has to give a certificate to the kernel.
This makes obvious the gap between proof assistants providing formal guaranties, and state-of-the-art automated tools the results of which have to be relied upon.
The aim of Project A3PAT is to fulfil the important need for externalisation of proofs using rewriting techniques. We expect to achieve this aim in particular by defining generic ways of expressing certificates of reasonable size for possibly complex properties.
This amounts to:
In the middle term, we wish to implement our solutions into a new version of the CiME rewriting tool which should be able to produce mechanically checkable traces, for instance by the Coq proof assistant.