State of Proof Checking

[andrewjlawrence]

I am interested in using Z3 in safety critical applications which necessitates having a proof checker of some kind. Is the work on DRAT(T)/DRUP(T) done or is there any further work needed for this to be useful? Would that be the recommended proof format for checking?

[NikolajBjorner]

It is very much up for grabs. I try to shop the project around for potentially interested parties.
I use a built-in self-bootstrapped checker to find bugs.
The self-bootstrapped checker can be used as a starting point for an external solid checker:
it contains the different cases for parsing the log and what they mean.
It is in shell/drat_frontend.cpp.

Note that the DRUP(T) proof logs are for a "new" core which is only selectively exposed for testing at this point.
It is the long game to have this the default but requires bug fixes, perf fixes and features (strings are missing).
The value of creating a DRUP(T) checker at this point is first of all going to be on advancing proof tool techniques
(profiling, visualization, feature extraction, trimming, core extraction, interpolation).

[andrewjlawrence]

My employer Siemens Mobility is interested in helping out and improving this area. We will have a discussion internally and then get back to you, possibly in private via email.

[nunoplopes]

Nice! 🥳

[NikolajBjorner]

The format for DRUP(T) proof logs is evolving and getting more usable.

A commit message describing curent activities is here: 107981f

[andrewjlawrence]

Thanks Nikolaj, this is very helpful and will provide us with a good starting point. The PhD student we have funded to look into proof checking will now start work in January as he is currently writing his masters thesis.

[NikolajBjorner]

A set of updates are being added this week to z3 to enable proof logging and checking. Specifically self-validation.

• https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES.md
• https://github.com/Z3Prover/z3/blob/master/examples/python/prooflogs.py
• https://github.com/Z3Prover/z3/blob/master/examples/python/proofreplay.py

The first use of these updates is to make it easier to debug development of z3.
They are also aimed to enable several scenarios as described in the release notes.
Proof checking will remain wide open ended and there are several places to include
external integrations and contributions.

The slides, https://z3prover.github.io/slides/proofs.html summarize some of the motivations and designs.

[andrewjlawrence]

@NikolajBjorner I had a meeting with the proof checking PhD student last week where we came up with a very high level plan for the PhD. Would you be interested in coordinating/aligning in anyway? We could do a bunch of work and then make a merge request after some time but I can see us doing redundant work or not doing things in a way that fits in with the rest of Z3.

[NikolajBjorner]

Of course, please don't hesitate to set up a call.