A brief report on FLOC

I was visiting this year the very large FLOC conference (2 weeks, 2000 visitors, <org>). The main topic of discussion was artificial intelligence (AI). Many talks were related to new applications and new scenarios of use of these kind of technology. Quite a number of very critical issues have been raised: how can we manage the mass of information ? What about security, privacy, authorship? How to handle the flood of autoformalisations? How to motivate the youngsters to really learn programming?

Three keynotes stood in my view out in this particular conference.

Leonardo de Moura gave a keynote presenting recent developments around Lean in a very enthusiastic manner. However, in my view, the talk gave very little credit to earlier work in interactive theorem proving and to the systems and ideas on which Lean builds. His attitude "We invented Interactive Theorem Proving" (with the exception of Daphne, perhaps) was understandably provocative on a conference like FLOC. Problems with AI ? Teething problems !! This will all work out, and we live in exciting times with a great future !!! In the midst of the quite controversial debate around this talk, a Lean kernel soundness bug was reported in connection with an AI-assisted purported disproof of the Collatz conjecture. According to Leonardo de Moura’s postmortem, the generated development exploited a bug in the kernel’s handling of nested inductive types. [HOL4 or Isabelle don't handle Induction in the Kernel at all; Isabelle had in the last 40 years 5 Kernel Bugs...]
Another outstanding keynote was given by David Mulligan who presented ongoing work on a hypervisor verification project on Isabelle/HOL, Nitro Isolation Engine: Formally Verifying a Production Hypervisor. David was referring to major breakthroughs in this verification project due to AI: hundred thousands of lines have been generated and the speed of verification has dramatically increased. According to him, the bottleneck is nowadays not so much doing the proofs, the bottleneck is to find experts who drive the AI in the right direction, who find the right modeling and who can recognize what is good and what is bad in generated autoformalisations.
On the Isabelle workshop happening just before the ITP conference, Larry Paulson gave a Keynote "Isabelle: the last 40 years (and the next)" (Isabelle is actually older than Linux!). During the workshop, several applications and tools were presented. In particular, there is an Isabelle MCP (a deep connector of the Isabelle PIDE) that works together with various LLMs like Claude or Gemini and interacts closely with Isabelle see the Zenodo repo.

Using Claude for Isabelle : My Experiences

I have started to use Isabelle with Claude Code, Claude Sonnet 5. I have not tried yet another LLM: for me it is crucial to design a thread, in advance, in order to drive the LLM in the good development direction. Claude seemed most appropriate to me (program development oriented, proof-oriented, Isabelle-ophile) to learn about this activity. But this is my personal choice.

Usage and Security

I create a sandbox (a directory in which I put any relevant sources, links to theories, prototypes, proofs for special cases, proof-sketches, and a ROOT (Isabelles Project configuration file.) Then I start the dialogue (the 'thread' or 'chat') in which I declare in natural language the objective, the ressources, and the access rights. I observed that Claude sometimes attempts to modify Isabelle and my OS hinders it; my colleague Achim Brucker (Chair of Computer Security U. Exeter and much more pecky than I am) creates an entire User at OS level to insure separation. With my setup, I started 2 developments in independent threads.

Case Study: A Proof Attempt in HOLCF and HOL-CSP

I first asked Claude to generalise a proof in the development version of HOL-CSP 2.0. My initial problem was to explore the link between the process-algebraic definition of deadlock-freeness (based on refinement):

   deadlock_free P ≡ (μ x. ⊓a∈UNIV → x) ⊑ P

to a co-inductive scheme like:

   (⋀x. x ⊑ P ⟹ ⊓a∈UNIV → x ⊑ P)  
    ⟹ deadlock_free (P)

(if from some state x which refines P any direct successor state does not block and refines P, then P is deadlock free.). Seen operationally, this corresponds to an argument that there is no blocking in a so-called "lasso" of length one.

Having already established a proof for this formulated directly in terms of process algebra, I knew that a generalisation to lasso-length n would be tedious but feasible. I asked Claude whether it could generalise to lassos of arbitrary finite length n (I also stated the lemma).

After several attempts, I was nearly giving up. But then after a final attempt Claude came back with a proof that actually stunned me. Instead of reasoning directly about processes, it followed an approach that is based in the underlying Scott-domain theory of HOLCF. Using this general result (not known in the library) about the least fixed points of continuous functions, it established desired co-induction principle:

     (⋀x. x ⊑ P ⟹ ⊓a∈UNIV → ((λ X. ⊓a∈UNIV → X)^^n) x ⊑ P)  
     ⟹ deadlock_free (P)

The fact that surprised me most was that Claude used as key insight the universal Kleene-Theorem:

(aⁿ)∞ = (aᵐ)∞

presented in the abstract setting of Scott-Spaces rather than staying on the level of process algebras (see the proof of this core theorem below.)

Which is clearly more abstract, and therefore more insightful.

It was easy to go from there and prove variants of these co-induction schemes: deadlock freeness for potentially terminating processes, lifelock freeness for terminating a non-terminating processes, etcpp.

Discussion:

Q: How does one know that the formalised definitions correspond what you have in mind?

A: Well, that's the universal validation problem of a formal theory, based on

  some definitions. Physicists set up experiments, Mathematicians set up
  characterising properties (desired properties that the concept should have,
  in particular in corner cases...) and Computer Scientists set up proofs (for
  corner cases) or tests. With respect to notations and technical problems to
  set up such "tests of a theory", I am willing to help.

Q: What is the quality of the proofs ?

A: Well, there is a tendency to make detours and repetitions, and not to

  recognise an invariant in many similar cases. First human proof attempts have
  that too. However, the overall code-quality is surprising, and the maitrise
  of Isabelle's mechanisms to link notations to semi-formal explanations is
  amazing. The example proof below of the key-theorem is structured as 
  a "calculational declarative proof" that looks **exactly** like one you'd find in a 
  textbook or in the slides of a talk:

lemma fix_funpow_eq:
    fixes f :: ‹'a::pcpo ⇒ 'a›
    assumes cont_f: ‹cont f›
    shows ‹(μ x. (f ^^ Suc n) x) = (μ x. f x)›
proof -
    define g where g_def: ‹g ≡ f ^^ Suc n›
    have cont_g: ‹cont g›
      unfolding g_def by (rule cont_compow[OF cont_f])
    have ‹(μ x. g x) = (⊔i. (g ^^ i) ⊥)›
      by (simp add: fix_def_alt'[OF cont_g])
    also have ‹… = (⊔i. (f ^^ (Suc n * i)) ⊥)›
      unfolding g_def by (simp only: funpow_mult)
    also have ‹… = (⊔k. (f ^^ k) ⊥)›
      by (rule lub_cofinal_compow[OF cont_f])
    also have ‹… = (μ x. f x)›
      by (simp add: fix_def_alt'[OF cont_f])
    finally show ?thesis unfolding g_def .
qed

The overall proof of the generalised co-induction scheme involved 4 lemmas, each of which requiring an own induction. So, this involves strategic planning and goes way beyond "sledgehammer", which is still useful to fill in gaps which I used to eliminate broken minor proof steps.

Case Study: A "From-Scratch-Redesign" of an Isabelle Plugin

This case study involved deep programming insight into Isabelle core and and a feeling for existing programming practices. It touches areas (producing on-screen markup, nitty-gritty details of the parallel execution engine) which are not very well-documented and require some experimenting: one can see this as an exercise in developing a complete redesign of an existing prototype.

In particular, the prototype is called "Isabelle/C" and it is available on the Isabelle/AFP; Isabelle/C already exists, as the Isabelle/C AFP entry, described in Tuong and Wolff, Deeply Integrating C11 Code Support into Isabelle/PIDE, F-IDE 2019.

Isabelle/C is a front-end that lets C11 source text live inside an Isabelle theory as a first-class citizen: parsed by a real grammar, checked incrementally under Isabelle/PIDE (so a syntax error, an undeclared identifier, or a malformed annotation is reported exactly like any other Isabelle error, with the usual jEdit markup, hyperlinking, and hovering), and open to attaching arbitrary Isabelle-level content (proof obligations, HOL terms, arbitrary Isar commands) to specific points in the C source via a comment-based antiquotation mechanism. It is not a C compiler, nor a verification tool in its own right: it is the front-end layer of a verification tool, a documentation generator, or a static analysis that would be built on top of it. However, it is based in large parts on very redundant generated SML code which turned out to be difficult to maintain and to extend.

My objective was to create Isabelle/C Version 2 built on ml_lex_yacc, Isabelle/AFP’s own generic, off-the-shelf ML-Lex/ML-Yacc integration for Isabelle/HOL (based on ’Main’) rather than the hand-crafted mix of generated lexer and parser sources of Version 1. It is not a port of the AFP entry’s code, and does not depend on it; it exists to answer a narrower question: how much of the essence of the Isabelle/C approach (inline and file-based parsing commands, antiquotation-carrying comments, an environment tracking declarations across a translation unit, programmable handlers) can be reproduced on top of a generic parser-generator toolkit, while simplifying the original design that experience showed to be disproportionately complex. Since the lexer-part of version 1.0 was effectively based on a version-split from Isabelle2019, the maintenance of Isabelle/C version 1.0 turned out to be problematic at various occasions in the Isabelle AFP development.

So I set up the sandbox with initially just the links to the Isabelle/C VS 1 project and the reference to the accompanying paper. I put in the sandbox the call file of the original implementation notably at 22 kLoc long generated SML file containing among many other things the abstract syntax (AST). The entire VS 1 is about 100 kLoc, on top of the AST.

The first part of the exercise was to reduce this module to a reasonable size. Claude was able to make a dependency analysis on this source and detect large parts which were actually irrelevant and that could be eliminated (this particular file shrunk to just 900 lines). Other parts were related to the issue that curried and un-curried versions of the AST that have been provided in order to make the original generating tool chain work. The C11 grammar, taken form the net, was automatically converted into the format `Isabelle_lex_yacc` required, and the link to the purified AST was equally quasi automatic, together with pretty-printer generations.

Note: I am not aware of any other tool that could provide for SML this; the ability of LLM-s to convert between languages and language paradigms plays obviously a crucial role here.

The next phase - constructing an environment for the generated ASTs in order to establish the declaration-use links on the interface involved for me the necessity to program certain examples and code-snippets myself; Claude extended this for the entire language by asking me a number of design-decisions occurring this generalisation.

I sketched in natural language the core algorithm for navigation strings (see the [rd], [rrd] below, that steer the effect of the C-Antiquotations, in particular highlight, that is applied to the specified part of the compiled AST):

Claude reacted with a number of questions clarifying corner-cases of my description, stated at some point "now I know everything" and implemented the 150 lines of the algorithm in about 30 sec.

Claude's debugging capacity impressed me most. It can not "see" what is happening on my screen, but from my descriptions it inserted assertions in the code and analysed the resulting debug-traces to find error-patterns in the GUI behaviour. And used this for corrections. I rediscovered testing: Chapeau!

At the end, after one week, a thread of about 300 pages pdf long was created. Claude abstracted from that a manual (not perfect, but a good basis for my own redaction). The entire code base is reduced to ~9kLoc of fairly readable SML code. The known limitations are that Isabelle/C VS 2 is no longer fully compliant to the C11-Standard (what VS 1 was except some aspects of CPP behaviour), and that the current implementation is not reentrant due to heavy side-effects in the Lex-Yacc-generated code.

Resume: It is not at all the case that Claude resolved all my dreams "automatically". Without the experience of the prior prototype VS 1 and my knowledge on general Isabelle internals I would not have been able to bring Claude to this result. I constantly had to check the results, find bugs, describe error-patterns, correct documentations, simplify tests, detect design errors, lead a structured retreat from paths where the development ran into a wall, code some example snippets, and describe precisely what the objective is, what I actually WANT TO DO.

Is AI creative ?

On that level, in my experience, no.

Previous meeting -- Next meeting