CoreFi: An Orchestration Language for Embedded Systems - Bridging Implementation to Specification

Establishing the correctness of concurrent systems has been approached from two directions historically: top-down, where global specifications are projected into local implementations, such as choreographic programming, and bottom-up, where global specifications are extracted from implementations for verification. Neither direction has found a satisfactory answer, especially when computation and communication are deeply intertwined, and participants share state—as is common in embedded systems. We present CoreFi, a Communicating Sequential Processes (CSP)-inspired orchestration language that bridges low-level implementations (e.g., C) via computation events and top-level specifications via channel communication (with bounded buffers) and process composition, opening the door to automated formalisation and verification of the full implementation. CoreFi is short for Core Language of Fiducia, where the latter pursues secure by design through language-based information flow security.

About Dr. Alex Potanin

Alex completed his PhD on Generic Ownership, showing how type polymorphism can be used to provide ownership type support in any language. After a full-year sabbatical at Carnegie Mellon University working with Professor Jonathan Aldrich, Alex created the Wyvern Programming Language - a novel general-purpose language based on object capabilities and effects designed from the ground up with security and usability as its primary goals. This produced numerous publications including work on type-specific languages and decidable typing for type members.

Since joining the Australian National University in 2022, Alex's research has centered on trustworthy systems and quantum program verification. In particular, the Fiducia language for verified embedded systems building on the seL4 microkernel. He is a Permanent Member of IFIP Working Group 2.4, a Senior Visiting Fellow with the Trustworthy Systems group at UNSW Sydney, and leads the School of Computing's GenAI teaching deployment under the ANU–Anthropic partnership.