Thomas Gazagnaire

Yesterday evening I was at the first Thought Experiment, a new series of informal evenings on how "AI is changing the way we code, find vulnerabilities, and prove theorems". It was held at the Paris School of AI, which turns out to be a few hundred metres from the Tarides office, and it was cheerfully organised by Caterina Urban and Karthik Bhargavan, with whom we are sending formally verified post-quantum cryptography to space.

Message sequence charts for agents

Benedikt Bollig (CNRS, LMF) asked whether AI agents can be made to coordinate safely. I read his papers on message sequence charts (MSCs) during my PhD, when I was working on scenario languages built on the same formalism, so I was curious to see where he would take them twenty years later. The answer is agentic workflows. An MSC draws each participant as a lifeline and each message as an arrow between two of them, and that is a good fit for a system of agents: the message-passing structure around the LLM calls is where deadlocks and type-mismatched messages live, and that part can be checked. His paper with Matthias Függer and Thomas Nowak (ISoLA 2026) turns this into a small language in which every choice and every loop is decided by one named participant, who tells the others which branch was taken. A projection then generates each agent's local program from the global chart, deadlock-free by construction whatever the LLM calls return. There is a Python implementation called ZipperGen.

Writing an exchange down once and cutting out each participant's part has a long history, from the realisability of MSCs studied by Alur, Etessami and Yannakakis to the multiparty session types of Honda, Yoshida and Carbone; I spent a few years myself generalising these techniques to more abstract partial-order automata. They stayed in papers because a global specification is long and precise, the proof that an implementation follows it is longer still, and few projects could afford to write either by hand. Over the past year that cost has collapsed, because models now write the verbose parts. So the same ideas are resurfacing twenty years later, with concrete applications, and I find that fascinating.

I have also tried to revive those ideas recently, in a new framework I called ocaml-fsm (it now handles symbolic state machines too, so I should think of another name before a proper release :p). It is early days and very much a prototype, limited to Mazurkiewicz traces for now, with full pomset automata cooking. Used as an oracle, though, it has already found bugs in reviewed and tested code, such as a security association in our CCSDS stack that could be neither created nor deleted. Compared with Benedikt's agents, it works one level down, on the finite control of protocols such as HTTP/2, SSH or the CCSDS security layer, and at the same level in mq, my merge queue, where landing a branch is one description of the flow between the caller, the hook that admits the entry, the run that holds the lock and the resolver that takes its conflicts. The rule is one exhaustive OCaml function. The tool evaluates it over the finite domains of states and inputs, and reports the states the code can never reach and the arrows it can never take, each with the shortest sequence of messages that shows it. Fsm.Global.project does the projection, cutting each party's machine out of one description of the whole exchange, on the boxed-pomset theory Loïc Hélouët and I worked out in 2007 (so the talk felt like familiar ground). A keepalive protocol is written once for both parties, one arrow per message, and the sender of a message the standard leaves optional is the one who decides:

let keepalive ping =
  Fsm.Global.v ~name:"keepalive" ~initial:Fresh ~roles:[ Client; Server ]
    ~pp_role ~controls:[ Fresh; Live; Over ] ~pp_control:pp_phase
    ~arrows:
      [
        Fsm.Global.arrow ~sender:Client ~receiver:Server Hello;
        Fsm.Global.arrow ~sender:Client ~receiver:Server Ping;
        Fsm.Global.arrow ~sender:Client ~receiver:Server Bye;
      ]
    ~pp_message ~error:pp_error ~finals:[ Over ]
    (fun phase (arrow : (role, message) Fsm.Global.arrow) ->
      match (phase, arrow.message) with
      | Fresh, Hello -> Fsm.goto Live ~effects:[]
      | Fresh, (Ping | Bye) -> Fsm.refuse Not_open ~effects:[]
      | Live, Hello -> Fsm.refuse Busy ~effects:[]
      | Live, Ping -> ping ()
      | Live, Bye -> Fsm.goto Over ~effects:[]
      | Over, (Hello | Ping | Bye) -> Fsm.refuse Finished ~effects:[])

Fsm.Global.project then gives each party its own automaton. The client may send a ping or not; the server takes it whenever it comes.

# let () = show_party Client "send ping to server";;
live on send ping to server: goto live
live on send ping to server: reject quiet
latitude on send ping to server in live: Example 5.1, recommended false
# let () = show_party Server "receive ping from client";;
live on receive ping from client: goto live
no latitude

The realisability check runs when the description is built, so a test that constructs it is enough to catch it (the types do not, yet). If accepting the ping could lead to two different phases, the server could not tell from the message which one the client chose, so the constructor refuses the description. The message names the cell, the ping at live, and the two phases, live and over, that the receiver would have to choose between without being told.

keepalive (fun () ->
    Fsm.may ~clause:"Example 5.2"
      [ Fsm.goto Live ~effects:[]; Fsm.goto Over ~effects:[] ])

Proofs on machine code, and the oracle problem

Úlfar Erlingsson (Google Cloud Security) had the best title of the evening, "Petrifying the dungheap: Better software through bookkeeping". His starting point is that finding bugs has become so easy that the software we all build on stands revealed as a dungheap. We see it in the OCaml ecosystem too, from two directions. The frontier models now write OCaml well (a few of us wrote last year about what it would take), so the bug and security reports reaching the OCaml compiler and the libraries around it have become noticeably better, and a report now tends to come with a patch that compiles and a test that fails without it. And Scrutineer, Andrew Nesbitt's agentic scanner, finds plenty: by the end of September a dozen OCaml developers were triaging on Anil's instance and twenty-four fixes had been merged in ocaml-tls, ocaml-x509, mirage-crypto and others. Type safety definitely helps here, but there is still a surprising number of bugs lying around in our nice OCaml libraries.

Úlfar's bookkeeping is for the code that cannot be rewritten in a safer language, because its performance and memory footprint have to stay where they are, and because even its bugs are part of its contract: fix one and something that relied on it breaks. The idea is to prove pre- and post-conditions directly on the machine code, with neither the source nor the compiler in the trusted base, and to use the proofs to find memory-safety bugs in software as it ships. The proofs are generated, which raises the question every generated artefact raises: is the program the proof was built for the program that ships? His answer is the cheapest oracle there is, a byte-for-byte comparison of the generated binaries.

I met the same question porting Tailwind to OCaml, where models wrote much of the code. The first check was bytes against the reference compiler's output, then a CSS-aware diff, because the reference emits spellings that differ without mattering. But a model can change a test and the code it checks in the same commit, so the check that decides has to share no code with either tool. In my case it is Chrome rendering both stylesheets and comparing pixels. Úlfar's bytes and my pixels do the same job. Once a model generates the artefact, the oracle has to sit outside anything the model can touch, and the simpler it is, the easier it is to trust.

AI tools for democracy

Lê Nguyên Hoang (Télécom Paris) closed with "AI tools to democratically govern AIs". He started from the attacks: AI is being used against democracies everywhere, in disinformation and in the recommendation systems that amplify it. His point is that the same tools can make democracies harder to attack, with better recommender systems and tools for building consensus, and Taiwan's g0v civic-tech community was his running example. (He is also behind Tournesol, a participatory recommender.) I am halfway through Plurality by Glen Weyl and Audrey Tang, so the talk landed on prepared ground.

It also made me finish a small thing I had been playing with, a page on French public money that lays out the official figures, each number linking to the Eurostat or Insee cell it came from and the arithmetic in between. It is a visualisation tool and nothing more. I have a few other ideas for this kind of data (one of them is a map of every commune, below), and I will write about them if they become something.