Re: [isabelle] soundness of Isabelle/HOL

Hi all,

  Matt Kaufmann and I ran a workshop on topics related to this issue
(Trusted Extensions of Interactive Theorem Provers). See

for the homepage and

for a summary of the techniques.


On Mon, Jan 30, 2012 at 9:35 AM, "Mark" <mark at> wrote:
> That's right, what I didn't say was that proof checking can address many of
> the remaining soundness-related vulnerabilities (and HOL Zero is very much
> intended to be used in precisely this way, as a proof checker).  For
> example, any concern that the datatype for theorems is being overwritten by
> the proof script can be addressed by recording the proof and exporting it to
> another system.
> But this proof checking can still suffer problems if the system importing
> the proof is not suitably trustworthy.  For example, if both systems have a
> pretty printer that have the same vulnerability (e.g. not distinguishing
> between two overloaded HOL variables), then the problem won't get noticed in
> either system.
> Mark.
> on 30/1/12 2:50 PM, Randy Pollack <rpollack0 at> wrote:
>> A well known approach to soundness, not discussed here yet, is
>> independent checking.
>> As Larry points out, a user must read and understand the statements of
>> theorems s/he wants to believe, and all definitions they hereditarily
>> depend on.
>> Further there must be confidence that whatever form these theorems are
>> presented in is correctly captured by a proof tool's internal
>> representation (issues of printing/parsing/overloading, etc).
>> But the actual proofs are no cause to worry, at least in principle, at
>> least in a system like Coq or Isabelle that can produce complete,
>> independently checkable proof scripts. in some completely unambiguous
>> notation.
>> Randy Pollack
>> --
>> On Mon, Jan 30, 2012 at 7:59 AM, "Mark" <mark at>
> wrote:
>>> Larry, you rightly point out that there are more important worries for
>>> theorem prover users.  But this doesn't mean that soundness-related
>>> vulnerabilities should be ignored now.
>>> And also, importantly, I would say that theorem proving hasn't yet
> reached
>>> its potential.  Nowadays formal proof is largely confined to university
>>> departments and a handful of reputed specialist companies.  If/when
>> theorem
>>> proving does become big, commercial realities mean that there will be
>>> considerable outsourcing of proofs to contractors.  Undoubtedly
> commercial
>>> pressures will tempt some contractors to maliciously exploit
>>> soundness-related vulnerabilities, and so we should be taking steps now
> to
>>> address this.  I'm sure there would have been many in 1970s/80s
>> pooh-poohing
>>> the risk of computer users exploiting security-related vulnerabilities.
>>> Mark.
>>> on 30/1/12 11:51 AM, Lawrence Paulson <lp15 at> wrote:
>>>> Forgive me if I launch into my usual lecture: I have never seen a piece
>> of
>>>> work spoilt by soundness bugs in a theorem prover. I have seen many
>> pieces
>>>> of work spoilt by unrealistic models, incorrect axioms or proofs of
>>>> irrelevant properties. Soundness is vital, but (contrary to a widely
> held
>>>> belief) it doesn't absolve users of the need to know what they are
> doing.
>>>> Larry Paulson
>>>> On 30 Jan 2012, at 09:59, Matthias Schmalz wrote:
>>>>> Hi,
>>>>> Out of curiosity and for my thesis introduction, I have the following
>>>> question.
>>>>> I am wondering whether there is a theorem prover out there that gives
>>>> stronger soundness guarantees than Isabelle/HOL and whether there is
>>>> empirical evidence showing that the difference is practically relevant.
>>>>> I would also like to know when the last unsoundness bug in Isabelle's
>>>> inference core has been observed.
>>>>> I already know that Isabelle follows the LCF approach and that HOL is
>>>> built from a modest number of axioms using conservative extension
>> methods.
>>>> It is therefore very likely that proofs by Isabelle are correct. I also
>>> know
>>>> that this soundness guarantee is restricted to the inference core; for
>>>> example, nothing prevents users from configuring the parser to parse
>>> "False"
>>>> as "True" and therefore giving the impression that "False" can be
> proved.
>>>> (And of course, soundness rests on the assumption that compiler, ML
>>>> libraries, operating system, and hardware behave correctly.)
>>>>> Many thanks in advance,
>>>>> Matthias

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.