In Development

Secure by construction,
not by coincidence.

Fiducia is a programming language and toolchain for building verifiably secure systems on the seL4 microkernel. It brings formal verification to everyday developers—no PhD required.

Get in Touch See code examples

Under active private development. Public release planned for mid-2026.

Why Fiducia

Security and correctness, built in.

Fiducia closes the trust gap between the formally verified seL4 kernel and the applications built on top. It catches entire classes of bugs at compile time that would be invisible at runtime.

Choreographic Programming

Describe the global communication protocol once. The compiler projects it into correct local programs for each protection domain—deadlock-free by construction.

Information Flow Security

A two-level security type system (Low/High) statically enforces that sensitive data never leaks to lower-security domains. No runtime checks needed.

Deadlock Freedom

Five well-typedness conditions—unique ownership, paired communication, acyclic channels, and more—guarantee that every well-typed choreography is deadlock-free.

CSP-Inspired Processes

Program protection domain behaviour using communicating sequential processes with events, guarded choice, and channel send/receive—clear, composable, and verifiable.

seL4 Microkit Native

First-class support for protection domains, shared memory regions, typed channels, and the seL4 Microkit System Description Format. Compile directly to SDF.

Rust-Powered Compiler

A fast, modern compiler built in Rust with rich error diagnostics, LSP integration, and sub-microsecond compilation stages. Includes VS Code support.

By Example

Two files. One verified system.

A Fiducia project consists of a system declaration (.fis) that defines the global architecture, and per-domain programs (.fi) that describe local behaviour. The compiler verifies the whole.

System Declaration datadiode.fis 
// Memory regions used as channel buffers
MemoryRegion eth_outer_output(0x200_000);
MemoryRegion eth_inner_input(0x200_000);

// Protection domains: (priority, irq, budget, period)
ProtectionDomain eth_outer(99, 159, 1000, 100_000);
ProtectionDomain eth_inner(199, 155);
ProtectionDomain dd(100);

// One-way SPSC channels
Chan o2d = eth_outer --> dd;
    o2d.set_buffer(eth_outer_output);
Chan d2i = dd --> eth_inner;
    d2i.set_buffer(eth_inner_input);

// System composition
System = eth_outer ||| eth_inner ||| dd;
Data Diode Process dd.fi 
import "ddiode.c" as dd;
() : dd.init();

Process:
  Notified():
    o2d?pkt -> d2i!pkt -> Notified();
Ethernet Driver eth_outer.fi 
import "eth.c" as eth;

Mapping ring_buffer  (0x10_000, rw);
Mapping packet_buffer(0x200_000, rw);

Events:
  Event handle_irq:    eth.handle_irq(eth)
  Event restart_engine: eth.restart_engine(eth)
  Event send_frame:    eth.send_frame(pkt)

Process:
  Notified():
    irq?159 -> Handle_eth(); Notified();
Information Flow Checking security labels 
// Security labels prevent data leaks at compile time
High MemoryRegion secret(0x1000);
Low  MemoryRegion public(0x1000);

High Mapping m1(secret, "rw");  // OK: High -> High
High Mapping m2(public, "rw");  // OK: Low  -> High
Low  Mapping m3(secret, "rw");  // ERROR: High -> Low leak!
Compilation Pipeline

From specification to verified system.

The Fiducia compiler discovers your project files, parses them into a rich AST, validates cross-references and memory layout, checks information flow security, and emits a verified seL4 Microkit System Description.

.fis + .fi
Source files
→
Parse
Build AST
→
Validate
Cross-refs
→
Typecheck
Info flow
→
Lower
SDF IR
→
.system
seL4 Microkit

Where Fiducia fits in the verified stack

Application Protection Domains (C / Pancake)
↑ orchestrated by
Fiducia — Choreographic Specification & Verification
↓ compiles to
seL4 Microkit — System Description Format
↓ runs on
seL4 — Formally Verified Microkernel
↓
Hardware (AArch64)
Killer Applications

Security patterns you can verify, not just hope for.

We are building a library of verified security design patterns on seL4—currently implemented in C, these will be converted to Fiducia .fis and .fi specifications with compile-time security guarantees.

☞ Click any tile below to explore the full example—including architecture diagrams, C implementations, and Fiducia code.

Information Flow
Fiducia Example

Network Data Diode

Enforces strict one-way information flow between HIGH and LOW networks through a trusted intermediary. The diode applies policy checks and audit logging—no data ever flows backwards.

Content Policy
Fiducia Example

Clipboard Guard

Inspects clipboard content crossing domain boundaries against a policy (e.g. rejecting "TOP SECRET", "CLASSIFIED" keywords). Only approved content is forwarded, with full audit logging of every decision.

Multi-Level Security
Fiducia Example

MLS Email Guard

Manages asymmetric email flow between SECRET and OFFICIAL domains. Downgrade: allowed after sanitisation (stripping classified markers). Upgrade: always blocked. The guard enforces the policy, not the user.

Trusted Input
Fiducia Coming Soon

Keyboard Switch

Routes HID input to one security domain at a time with buffer flush on switch. Keystrokes are delivered exclusively—no broadcast, no residual data leakage between SECRET and UNCLASSIFIED domains.

Trusted Display
Fiducia Coming Soon

Framebuffer Compositor

Multiple security domains render to isolated framebuffers. A trusted compositor reads all buffers and draws border decorations that cannot be spoofed. Domains cannot read each other's display content.

Covert Channels
Fiducia Example

NRL Pump

A probabilistic downgrader that buffers, reorders, and adds timing jitter to messages crossing security boundaries. Defeats timing-based covert channels that simple data diodes leave open.

Residual Data
Fiducia Coming Soon

Domain Switch Flush

Zeroes all shared workspace buffers on every domain switch, verified clean before the new domain activates. Prevents covert channels through residual state in shared memory.

Virtualisation
Fiducia Example

Linux VM Data Diode

Ethernet-level data diode between two full Linux virtual machines running on seL4. Frames flow HIGH→LOW only through a trusted bridge. The VMs are completely isolated by seL4 capabilities.

Media Sanitisation
Fiducia Example

JPEG Metadata Filter

Strips EXIF, GPS, camera data, and comments from JPEG images crossing a security boundary. Only pixel data passes through. Operates inline between Linux VMs at wire speed.

9
Verified security patterns and growing
seL4
Formally verified microkernel foundation
<4µs
Full compilation pipeline (per file)
The Australian National University
School of Computing, ANU
Supported Hardware

Verified systems on real hardware.

Fiducia targets AArch64 platforms supported by seL4. We currently develop and test on these boards, with more architectures available to industry partners.

AMD Kria K26I
Industrial-grade Zynq UltraScale+ MPSoC with quad-core Arm Cortex-A53, 4GB DDR4, 16GB eMMC, and on-board TPM. Designed for smart city, machine vision, and edge AI applications.
NVIDIA Jetson Orin
Up to 275 TOPS AI performance with Arm Cortex-A78AE CPU and Ampere GPU. Power-configurable 15–60W. Available in AGX, NX, and Nano form factors for robotics, autonomous systems, and edge computing.
More Architectures?
We can add support for additional AArch64 and RISC-V platforms. Join us as an industry partner to bring Fiducia to your hardware.
Research

Grounded in rigorous mathematics.

Fiducia builds on decades of research in choreographic programming, process algebra, and information flow security. Its theoretical foundations are published in peer-reviewed venues.

ChorFi: A Choreography Language for Embedded Systems

The first choreographic programming language designed for seL4 MicroKit. Formal operational semantics and a well-typedness discipline that guarantees deadlock freedom for any well-typed choreography. Draft coming to arXiv soon.

Formal Verification for Critical Systems

Fiducia makes advanced formal methods accessible to everyday developers. By embedding verification directly in the toolchain, it closes the trust gap between verified OS kernels and real-world applications.

Team

The people behind Fiducia.

Fiducia is built by a team at The Australian National University combining expertise in programming languages, formal methods, and systems security.

Alex Potanin
Lead
A/Prof Alex Potanin
The Australian National University
Expert in programming languages, memory and data safety. Creator of the Wyvern programming language. Research has influenced the design of Rust.
Yan Liu
Researcher
Dr Yan Liu
The Australian National University
Formal methods and model checking. PhD from National University of Singapore. Industry experience in formal verification at Runtime Verification and Pi Squared.
Alwen Tiu
Researcher
A/Prof Alwen Tiu
The Australian National University
Computational logic, automated theorem proving, and computer security. Internationally recognised research in mathematical proofs for trustworthy software.
Supporters

Backed by leaders in trustworthy systems.

Fiducia is developed at ANU with support from leading organisations in verified systems and space technology. We're looking for more partners to help shape the future of secure software.

Trustworthy Systems
Pioneers of the seL4 formally verified microkernel — the foundation Fiducia builds upon.
Skykraft
Australian space services company deploying small satellite constellations for air traffic management.
Your Organisation?
We're looking for industry and research partners to join us. Get in touch to collaborate.

Interested in trustworthy systems?

Fiducia is under active private development with a public release planned for mid-2026. Get in touch to learn more or discuss collaboration.

alex.potanin@anu.edu.au

Get in Touch