Introduction

Fiducia is a language for building embedded applications on seL4 Microkit systems. A Fiducia project describes a system of protection domains (PDs) connected by channels, each PD implemented by external C / Rust code and modelled by a CSP-style process algebra. From this single description the toolchain produces both a bootable Microkit image and a formal model that can be checked for deadlock-freedom.

This manual is the task-oriented guide to the toolchain. For the syntax and semantics of the language itself, see the Fiducia Language Reference — it stays focused on .fis / .fi syntax, while this manual covers installing, configuring, running, and verifying projects day-to-day.

🚧 Fiducia is under active development. The language and tools are not yet complete; interfaces described here may change between releases.

The toolchain at a glance

A Fiducia project

A project is a directory containing:

• one .fis file — the system description: memory regions, protection domains, channels, and the system composition;
• one .fi file per protection domain — the PD implementation: imports of C sources, memory mappings, event declarations, and process definitions (the file eth_outer.fi implements the PD named eth_outer);
• the imported .c implementation files (.rs imports parse but aren’t runnable yet — the C backend rejects them; see --emit=c);
• a fire.toml manifest telling fire how to build and run it (see The Project Manifest).

The compiler pipeline is:

discover → parse → resolve → validate → typecheck → WF2 → emit

where typecheck enforces information-flow security (no High→Low leaks via channels) and WF2 checks the channel dependency graph for cycles (a structural deadlock-freedom condition).

Where to go next

1. Install the tools.
2. Write or copy a fire.toml.
3. Build and run on QEMU — the demo/datadiode/ project in the repository is a complete worked example.
4. Verify deadlock-freedom.
5. Consult the fic reference for the individual compiler emit modes.

Installation

Fiducia ships two binaries: fic (the compiler) and fire (the project runner). They are not yet published to crates.io — install the pre-built binaries from the website.

Pre-built binaries (recommended)

Pre-built binaries are published monthly (and on manual dispatch) to fiducia-lang.github.io/releases. Available platforms: linux-x86-64, macos-arm64.

# Download and extract (replace <version> and <platform> accordingly)
curl -fsSL -o fic.tar.gz \
  https://fiducia-lang.github.io/releases/v<version>/fic-<platform>-<version>.tar.gz
tar -xzf fic.tar.gz

# Move to a directory in your PATH (the tarball contains both binaries)
sudo mv fic fire /usr/local/bin/
# Or for user-local installation
mv fic fire ~/.local/bin/

# Verify installation — fic and fire share one toolchain version
fic --version
fire --version

This manual and the language reference are published at fiducia-lang.github.io/docs/manual.

ℹ️ cargo install fic fire will become available once the project is published to crates.io after the language design stabilises.

Building from source

ℹ️ The source repository is private while the language is under development; building from source currently requires collaborator access.

git clone https://github.com/fiducia-lang/fic
cd fic
cargo install --path .       # fic
cargo install --path fire    # fire

The repository also provides a Nix flake (nix develop) that supplies the full toolchain — Rust, the Microkit SDK, and the cross-compiler — with no manual setup. See CONTRIBUTING.md.

Prerequisites for building images

Compiling a project to a bootable image (fire build, fire run, or bare fic — image generation is its default mode) needs the seL4 Microkit SDK and an AArch64 bare-metal cross-compiler.

Microkit SDK

# macOS (Apple Silicon):
curl -fsSL -o microkit-sdk.tar.gz \
  https://github.com/seL4/microkit/releases/download/2.2.0/microkit-sdk-2.2.0-macos-aarch64.tar.gz
# Linux (x86-64):
curl -fsSL -o microkit-sdk.tar.gz \
  https://github.com/seL4/microkit/releases/download/2.2.0/microkit-sdk-2.2.0-linux-x86-64.tar.gz

tar -xzf microkit-sdk.tar.gz

ARM GNU toolchain

# macOS (Apple Silicon):
curl -fsSL -o arm-gnu-toolchain.tar.xz \
  https://developer.arm.com/-/media/Files/downloads/gnu/15.2.rel1/binrel/arm-gnu-toolchain-15.2.rel1-darwin-arm64-aarch64-none-elf.tar.xz
# Linux (x86-64):
curl -fsSL -o arm-gnu-toolchain.tar.xz \
  https://developer.arm.com/-/media/Files/downloads/gnu/15.2.rel1/binrel/arm-gnu-toolchain-15.2.rel1-x86_64-aarch64-none-elf.tar.xz

tar -xJf arm-gnu-toolchain.tar.xz

QEMU (for fire run in QEMU mode)

Install qemu-system-aarch64 from your package manager (brew install qemu, apt install qemu-system-arm, …).

UPPAAL (for fire verify)

fire verify runs the UPPAAL command-line model checker verifyta. Download UPPAAL and either put verifyta on your PATH, set $VERIFYTA, or point to it from fire.toml. UPPAAL requires a (free academic) licence.

Environment variables

# Set once — add to your shell profile
export MICROKIT_SDK=<path-to-microkit-sdk>
export GCC=<path-to-arm-gnu-toolchain>/bin/aarch64-none-elf-gcc
export LD=<path-to-arm-gnu-toolchain>/bin/aarch64-none-elf-ld

Projects can instead pin these per-project in fire.toml’s [run.target] section.

The Project Manifest (fire.toml)

fire reads a fire.toml manifest from the project directory. It names the project, locates the sources, and configures how fire build / fire run build and execute the image and how fire verify invokes the model checker.

🚧 This page documents the manifest schema introduced with the fire build / fire run / fire verify subcommands (PR #174). Until that lands on a release, the previous [target] / [qemu] layout applies — see the CHEATSHEET.md of your installed version.

Complete example

[project]
name = "datadiode"     # output filename stem: build/datadiode.img / .xml
src  = "."             # directory with the .fis/.fi files, relative to this file

[run]
mode = "qemu"          # qemu | hardware (hardware is not yet implemented)
# Arguments for qemu-system-aarch64; {img} is substituted with the
# absolute path to the built image at runtime.
args = [
    "-machine", "virt,virtualization=on",
    "-cpu",     "cortex-a53",
    "-serial",  "mon:stdio",
    "-device",  "loader,file={img},addr=0x70000000,cpu-num=0",
    "-m",       "size=2G",
    "-nographic",
]

[run.target]
board   = "qemu_virt_aarch64"   # Microkit board identifier
profile = "debug"               # debug | release
# sdk / gcc / ld — optional, fall back to $MICROKIT_SDK / $GCC / $LD
# allow_wf2_cycles = true       # skip WF2 when `fire verify` covers deadlock-freedom

[verify]
mode = "verifyta"               # verification engine
# path / args — optional; path falls back to $VERIFYTA / PATH

[project] — identity and sources

[run] — execution mode and arguments

[run.target] — board and toolchain

When sdk / gcc / ld are set they are passed to the fic child process as environment variables, overriding any values already in your environment — useful for pinning a toolchain per project.

[verify] — formal verification

Optional section; configures fire verify.

Worked example

The repository’s demo/datadiode/fire.toml is a complete, runnable manifest for the data-diode demo — three protection domains (eth_outer, dd, eth_inner) built into one image and launched on qemu_virt_aarch64 with two virtio-net devices, driven from the host (demo/datadiode/inject.py) since a foreign-MAC diode needs raw frames a NAT can’t deliver.

Building and Running: fire build / fire run

fire build compiles a project to a bootable Microkit image; fire run builds and then launches it as configured in fire.toml — mimicking the cargo tools.

🚧 The build / run subcommands land with PR #174. On earlier versions the same behaviour is the bare fire <PROJECT_DIR> invocation.

Usage

fire build [PROJECT_DIR] [-o <IMG>]   # produce the image only
fire run   [PROJECT_DIR] [-o <IMG>]   # build, then launch

What it does

1. Reads fire.toml from PROJECT_DIR and resolves the source directory (project.src).
2. Builds the image — incrementally, like cargo: when build/<name>.img is already newer than every source file and fire.toml, the rebuild is skipped (✓ image up to date). Otherwise it invokes fic <src> --board <board> --build-profile <profile> (image generation is fic’s default mode), with the toolchain from [run.target] (or the MICROKIT_SDK / GCC / LD environment). This compiles each PD’s C file, patches the mapping setvars, and packs the loader, seL4 kernel, and PD ELFs into build/<name>.img. The freshness check is mtime-based — coarser than cargo’s fingerprints, but any source edit triggers a rebuild.
3. (fire run only) In mode = "qemu", launches qemu-system-aarch64 with the [run] args, substituting {img} with the built image path. mode = "hardware" is reserved and not yet implemented.

Walkthrough: the data-diode demo

$ fire run demo/datadiode/
fire: building datadiode for qemu_virt_aarch64 (debug)
  ✓ Parsed 1 system + 3 program files
  ✓ Resolved data layer (2 structs, 1 consts)
  ✓ Resolved names
  ✓ Resolved mapping vaddrs
  ✓ Type-checked information flow
  ✓ Checked channel dependency acyclicity (WF2)
MICROKIT|CAPDL SPEC: number of root objects = 84, spec footprint = 12.44 KiB
MICROKIT|INITIAL TASK: memory size = 412 KiB
MICROKIT|LOADER: image file size = 2.59 MiB
fire: launching QEMU ...

QEMU then boots the image; with -serial mon:stdio the PDs’ serial output appears in your terminal. Exit QEMU with Ctrl-A x.

To produce the image without launching:

fire build demo/datadiode/
ls demo/datadiode/build/datadiode.img

A Microkit build report is written next to the image at build/report.txt — useful for inspecting the memory layout and the setvar patches applied to each PD.

Troubleshooting

Verifying: fire verify

fire verify checks a project’s process-algebra model with the UPPAAL model checker. It emits a UPPAAL XTA model of the system (every PD’s processes as timed automata, channels as synchronisations), then runs verifyta and pretty-prints per-query PASS / FAIL results.

🚧 The verify subcommand lands with PR #174. On earlier versions the same behaviour is fic <PROJECT_DIR> --verify.

Usage

fire verify [PROJECT_DIR] [-q <QUERY_FILE>]

Writing queries

Queries are user-authored — which properties matter is application-dependent, so fic emits only the model and you state the properties. Write a UPPAAL query file named <name>.q next to your sources (it is part of the project, so commit it). The customary first line is deadlock-freedom:

/* the system never gets permanently stuck */
A[] not deadlock

/* the diode can complete a forward */
E<> dd.L1

Queries reference the process instance names from the emitted model (the PD names, snake_case) and template location names — inspect build/<name>.xml (or open it in the UPPAAL GUI) to find them.

What it does

1. Reads fire.toml and resolves the source directory.
2. Invokes fic <src> --emit=xta, writing build/<name>.xml (the UPPAAL model).
3. Locates the query file: the -q flag, or <src>/<name>.q. Errors if neither exists.
4. Locates verifyta — [verify] path → $VERIFYTA → PATH — and runs it with -t 0 (request a counterexample / witness trace), the model, the query file, and any [verify] args.
5. Parses the output and prints one PASS / FAIL line per query. Exits non-zero if any query fails.

Reading the output

$ fire verify demo/datadiode/
  ✓ Running verifyta: /opt/uppaal/bin/verifyta

  A[] not deadlock                          PASS
  E<> EthOuter.Handle_eth                   PASS
  ...

A failing query prints FAIL and, when verifyta produces one, the counterexample trace:

  A[] not deadlock                          FAIL
    Trace (12 steps):
      pd0.State0 → pd0.State1
      ...
      ↯ stuck at: pd0.State1, pd1.State2, ...

The ↯ stuck at line lists each automaton’s location in the deadlocked state — usually enough to spot the circular wait. A FAIL on a reachability query with (property unreachable — no counterexample trace) means the named location can never be entered.

Worked example: ping-pong

demo/pingpong/ ships two PDs (ping/pong) that bounce a bounded notification ROUNDS times over a genuinely cyclic channel (ping <-> pong), then go quiescent — a real case where WF2’s over-approximation would reject a topology that’s actually deadlock-free. Its hand-written pingpong.q states that, verified against the real emitted model (see tests/uppaal/pingpong/expected.xml for a known-good snapshot):

fire verify demo/pingpong/
#   A[] (deadlock imply ping.rounds == ROUNDS)   PASS
#   E<> ping.rounds == ROUNDS                    PASS
#   A[] ping.rounds <= ROUNDS                    PASS
#   E<> pong.L1                                  PASS

The first query is deadlock-freedom modulo intended termination: the only reachable quiescent state is the completed rally, so a blanket A[] not deadlock would itself report a false “deadlock” at the correct terminal state — see the header comment in demo/pingpong/pingpong.q for the full reasoning.

Ad-hoc queries

Pass a different query file for a one-off check — a per-invocation input, like a cargo test filter:

fire verify demo/datadiode -q queries/liveness.q

Relationship to the WF2 check

fic always runs WF2, a structural acyclicity check on the channel dependency graph, before emitting a deployable image. WF2 is an over-approximation: it rejects every cyclic topology, including systems that are deadlock-free under a fair scheduler (demo/pingpong’s ping <-> pong, for instance). When fire verify establishes deadlock-freedom, you can build such systems anyway with fic --allow-wf2-cycles — see the fic reference.

The fic Compiler

fic is the Fiducia compiler. fire drives it for the common build-and-run / verify workflows; invoke it directly to check a project, build an image with explicit flags, or inspect any intermediate representation.

fic <PROJECT_DIR> --board <BOARD> --build-profile <PROFILE> [-o <IMG>]   # image (default)
fic <PROJECT_DIR> --check                                               # front-end only
fic <PROJECT_DIR> --emit=<FORMAT> [-o <PATH>]                           # inspection emits

PROJECT_DIR is a directory containing exactly one .fis file and one .fi file per protection domain (bound by filename: eth_outer.fi implements PD eth_outer).

By default — like rustc, whose default output is a binary — fic compiles the project to a bootable Microkit image: it runs the full front-end, lowers to SDF, cross-compiles each PD’s C file, patches the setvars, and packs the loader, seL4 kernel, and PD ELFs into <project>.img. This requires --board / --build-profile and the MICROKIT_SDK / GCC / LD environment.

With --check, fic stops after the front-end — parse, data-layer resolution, name resolution, vaddr materialization, information-flow typecheck, WF2 acyclicity — and reports diagnostics without writing any output (the cargo check of Fiducia):

$ fic demo/datadiode/ --check
  ✓ Parsed 1 system + 3 program files
  ✓ Resolved data layer (2 structs, 1 consts)
  ✓ Resolved names
  ✓ Resolved mapping vaddrs
  ✓ Type-checked information flow
  ✓ Checked channel dependency acyclicity (WF2)

--emit formats

--emit replaces the default image output with an intermediate representation:

The inspection formats (rawast, ast, c, dot) skip the WF2 check — they have no deployment target. xta exists precisely to analyse cyclic systems, so it also skips WF2; image generation (the default) and sdf enforce it.

Options

--check

Run the front-end only; produce no artifact. Conflicts with --emit.

-o, --output <PATH>

Override the default output path for the image or the chosen emit mode.

--board <BOARD>, --build-profile <PROFILE>

Required for image generation (the default mode): the Microkit board identifier (e.g. qemu_virt_aarch64, kria_k26) and build profile (debug / release). Must match a directory under $MICROKIT_SDK/board/.

--allow-wf2-cycles

Skip the WF2 acyclic-channel-dependency check.

WF2 is a structural over-approximation: it rejects any cyclic channel dependency graph, including programs that are deadlock-free under a fair scheduler (e.g. the asymmetric dining philosophers, Hoare CSP §2.5.4). Use this flag when deadlock-freedom is established by an external authority — typically fire verify on the emitted UPPAAL model.

Language server

The Language Server Protocol server is a separate binary, fic-lsp (analogous to rust-analyzer vs rustc), built from the fic-lsp workspace crate and used by the editor integrations under editors/. Install it with cargo install --path fic-lsp; it speaks LSP on stdio.

Environment variables

Diagnostics

Errors are rendered as annotated source snippets with the offending span highlighted — parse errors, duplicate names, undeclared references, vaddr misalignment / overlaps, information-flow violations, and WF2 cycles all point back to the .fis / .fi source location.

Exit status

fic exits 0 on success and non-zero when any pipeline stage reports diagnostics, making it safe to use in scripts and CI.