Transpilation from Fiducia to Pancake

Build a Fiducia-to-Pancake transpiler inside HOL4: formalise Fiducia’s state machine intermediate representation (the Communicating Control-Flow Graph), implement its translation to Pancake as a HOL4 function, and prove the translation correct, so the verified CakeML/Pancake toolchain’s guarantee extends through this final step. Validate on real examples.

Picture of alex-potanin.md Alex Potanin

14 Sep 2026

Motivation

Fiducia is an orchestration language built on top of Microkit/seL4 that separates channel communication from low-level computation code, so that computation is orchestrated around communication events. It not only modularises embedded-system application design, but also enables auto-formalisation: extracting formal models, checkable by model checkers, directly from Fiducia code. However, to extend the formally verified source implementation to executable binary, a verified compilation toolchain is needed.

CakeML provides exactly this: a compiler implemented and verified entirely in HOL4, whose verified binary is produced via an in-logic bootstrapping technique — evaluating the proven compiler on its own source, inside the theorem prover — without needing to trust code extraction or an external compiler. Pancake is a systems programming language whose compiler is built on CakeML’s, inheriting the same end-to-end correctness guarantee, plus built-in Viper annotations for automated verification. It has already been used to produce verified device driver code in the same seL4/Microkit ecosystem Fiducia targets, with performance close to a hand-written equivalent — making it a natural translation target for Fiducia.

This project builds a Fiducia-to-Pancake transpiler, implemented, proved correct, and validated inside HOL4, so the strong correctness guarantee the underlying toolchain already provides extends all the way through this final translation step too.

Goal

Fiducia’s compilation is multi-stage, from a process-algebra-like syntax language to a state machine intermediate representation (IR) followed by code generation. However, to narrow the scope, this project targets the state machine IR — the Communicating Control-Flow Graph (CCFG) — to Pancake transpilation. Thus the goals are:

  1. Formalise the IR, CCFG, in HOL4 as a formal datatype along with its operational semantics;
  2. Implement the transpilation to Pancake as a HOL4 function, and prove its correctness;
  3. Validate the transpiler on real examples.

Bonus (attempt only if ahead of schedule after the core goal above):

  • Staying in sync. fic’s CCFG representation will keep evolving as Fiducia’s language grows — new constructs, new fields, new kinds of event. A HOL4 formalisation that mirrors CCFG’s exact current shape will drift out of sync with every such change, the same way any hand-ported specification does. How would you design the HOL4 side to absorb this gracefully — for instance, by defining a small, general transition-system semantics once, with CCFG treated as one instance of it, so that most future changes only touch the instantiation rather than the core semantics and whatever has already been proven about it?

Deliverable

  • A HOL4 formalisation of the CCFG intermediate representation: the datatype and its operational semantics.
  • The CCFG-to-Pancake transpiler as a HOL4 function, together with its correctness proof.
  • Validation of the transpiler on a set of real Fiducia examples.
  • The final report.

Requirement

  • Comfort with functional programming and formal/logical reasoning (experience with ML, Haskell, or a proof assistant such as Coq, Lean, or Isabelle is all relevant background) — prior experience with HOL4 specifically is not required.
  • Willingness to learn HOL4 under supervision. A HOL4 expert is available to support the formalisation and proof-adjacent work directly.

What you will learn

Formal-methods and engineering practice: faithfully representing an existing compiler’s internal representation inside a theorem prover, implementing a real translation in the same style an actually-verified compiler uses, and working alongside a formal-methods expert on a research-adjacent problem.

Take-home questions

  • Carrying annotations across: Pancake has built-in Viper annotations (preconditions, postconditions, invariants) that get checked automatically by an external SMT-based verifier. Fiducia’s events call out to downstream Pancake driver code, which may itself already carry such annotations. Can those downstream annotations be carried over into the generated orchestration code — perhaps via a separate tool implemented in Rust, rather than through HOL4?

References

arrow-left bars magnifying-glass xmark