Gale

Gale is a formally-verified Rust reimplementation of the Zephyr RTOS kernel primitives — semaphores, mutexes, queues, scheduler, and more — aimed at ASIL-D safety-critical embedded. The same primitives also compile to WebAssembly and dissolve to bare-metal native code (no runtime ships): that's gust, gale's smallest mini-OS, which runs on a tiny trusted native shim (just the mmio + irq capability). Verification runs on three independent engines — Verus (SMT/Z3), Rocq, and Lean. What "verified" does and does not cover is spelled out in the claims ledger; the honest bounds are below.

_{House jargon, once:dissolve = statically compile the wasm away into native so nothing interprets at runtime · meld → loom → synth = the dissolve pipeline (fuse components → inline → AOT-compile to the MCU) · thin-seam driver = a driver whose whole protocol is verified wasm importing only a small mmio capability (gust:hal) · TCB = trusted computing base, the native code you must trust.}

Build & test

Verification & dynamic analysis

Formally verified Rust replacement for Zephyr RTOS kernel primitives. ASIL-D targeted, triple-track verification: Verus (SMT/Z3) + Rocq (theorem proving) + Lean (scheduler/priority proofs).

Honest reading of "formally verified" (full claims ledger: docs/safety/verification-honesty.md): the proofs are on the Rust/wasm source — Verus SMT on 39 modules (subject to 133 named external_body trust units), 10 Rocq abstract-model invariant proofs (incl. the gust executor's no-lost-wakeups; poll/sched/thread_lifecycle are WIP Admitted stubs, not yet proven), and Lean scheduling theory. Two limits stated up front: (1) Rocq/Lean reason about abstract models, not the Rust directly; (2) the shipped artifact for the wasm-dissolve line is native code from meld→loom→synth and is differentially tested against a reference wasm semantics, not proven equivalent — there is no translation-validation yet, so "end-to-end verified pipeline" is not claimed. The engineering below is real; these bounds are what make each claim defensible.

Part of the PulseEngine toolchain.

Modules

39 Rust modules covering the full Zephyr kernel surface. All 39 pass Verus SMT verification (805 verified, 0 errors)¹:

¹ "Verified" here = the bodies Verus checked against requires/ensures contracts. Trusted-base inventory (133 #[verifier::external_body] shims + 2 assume_specification calls): see docs/safety/verification-honesty.md. The headline number is anchored by the formal-verification.yml CI job (bazel test //:verus_test); if that job is red, the number is stale until it goes green again.

Synchronization

Module	Zephyr Source	Properties	Status
sem	kernel/sem.c	P01-P10	Verified + Zephyr tested
mutex	kernel/mutex.c	M01-M11	Verified + Zephyr tested
condvar	kernel/condvar.c	C01-C08	Verified + Zephyr tested
spinlock	kernel/spinlock	SL01-SL05	Verified
futex	kernel/futex.c	FX01-FX06	Verified
atomic	kernel/atomic.c	AT01-AT06	Verified

IPC

Module	Zephyr Source	Properties	Status
msgq	kernel/msg_q.c	MQ01-MQ13	Verified + Zephyr tested
stack (k_stack)	kernel/stack.c	SK01-SK09	Verified + Zephyr tested
pipe	kernel/pipe.c	PP01-PP10	Verified + Zephyr tested
mbox	kernel/mailbox.c	MB01-MB06	Verified
fifo	kernel/fifo	FI01-FI06	Verified
lifo	kernel/lifo	LI01-LI06	Verified
queue	kernel/queue.c	QU01-QU06	Verified
ring_buf	sys/ring_buffer	RB01-RB08	Verified
poll	kernel/poll.c	PL01-PL08	Verified (external_body for array mutation)

Timing

Module	Zephyr Source	Properties	Status
timer	kernel/timer.c	TM01-TM08	Verified
event	kernel/events.c	EV01-EV08	Verified
timeout	kernel/timeout.c	TO01-TO08	Verified
timeslice	kernel/timeslice	TS01-TS06	Verified
work	kernel/work.c	WK01-WK06	Verified

Memory

Module	Zephyr Source	Properties	Status
mem_slab	kernel/mem_slab.c	MS01-MS08	Verified
heap	lib/os/heap	HP01-HP08	Verified
kheap	kernel/kheap	KH01-KH06	Verified
mempool	kernel/mempool	MP01-MP06	Verified
mem_domain	kernel/mem_domain.c	MD01-MD06	Verified
stack_config	arch/stack	SKS01-SKS05	Verified

Scheduling

Module	Zephyr Source	Properties	Status
sched	kernel/sched.c	SC01-SC16	Verified (external_body for array mutation) + Lean proofs
thread	kernel/thread.c	TH01-TH06	Verified
thread_lifecycle	kernel/thread.c	TL01-TL06	Verified
priority	kernel/priority	-	Verified + Lean proofs
wait_queue	kernel/waitq	-	Verified
smp_state	kernel/smp	SM01-SM04	Verified

Safety

Module	Zephyr Source	Properties	Status
error	kernel/errno	-	Verified
fatal	kernel/fatal.c	FT01-FT04	Verified
fault_decode	arch/fault	FD/FH01-FH03	Verified
device_init	drivers/init	DI01-DI05	Verified
dynamic	kernel/dynamic.c	DY01-DY04	Verified
userspace	kernel/userspace.c	US01-US08	Verified

Architecture

src/*.rs Verus-annotated Rust (39 modules, single source of truth)
|
+---> Verus verification (39/39 modules, 805 verified, SMT/Z3)
|
+---> verus-strip ---> plain/src/*.rs (auto-generated plain Rust)
| | |
| | +---> cargo test (unit + integration + proptest)
| | +---> Kani BMC (185 harnesses)
| | +---> clippy ASIL-D lint profile
| |
| +--standalone--> plain/*.rs ---> Rocq proofs (9 modules)
|
+---> proofs/executor_proofs.v ---> Rocq model proof (gust executor, no-lost-wakeups)
|
+---> proofs/lean/*.lean ---> Lean 4 proofs (3 files, scheduler + priority)
|
+---> ffi/ ---> C shim ---> Zephyr kernel (qemu_cortex_m3/m4f/m33)

Verification

Formal verification (via Bazel + Nix, CI-gated on source changes):

• Verus (SMT/Z3): 39/39 modules, 805 properties verified by Z3 (0 errors). Includes poll and sched with external_body trusted array helpers.
• Rocq: 10 fully-proven abstract invariant modules (0 Admitted): 9 over Z-valued math for the Zephyr primitives, plus executor_proofs.v — an N-bitmask model of the gust executor proving no-lost-wakeups (see below). NOT connected to the Rust code — proofs reason about hand-written mathematical models, not the rocq-of-rust translation. poll/sched/thread_lifecycle remain Admitted WIP stubs.
• Lean 4: 3 mathematical proofs — RMA bound, priority ceiling protocol, priority queue ordering. Pure scheduling theory, not implementation proofs.
• Kani BMC: 185 bounded model checking harnesses (87 model + 98 FFI). Not in CI until Bazel workflow is confirmed working.

Executor no-lost-wakeups: one property, three independent tracks

The gust executor's load-bearing liveness-support property — a wakeup delivered to a Pending task is never lost: its ready bit stays set across any interleaving of wake/consume/pick_next until that task itself is consumed — is discharged on all three verification tracks:

Track	Artifact	What it checks	Engine
Verus	src/executor.rs (lemma_no_lost_wakeup + per-mutator ensures)	the property on the Rust source itself	SMT (Z3)
Rocq	proofs/executor_proofs.v (no_lost_wakeups, delivered_wake_survives)	the property on a hand-written model of the same state machine, over arbitrary finite operation traces	Rocq kernel (type theory, no SMT)
Kani	src/executor.rs#[cfg(kani)] harnesses	the executable scheduler loop (drain + bounded-poll) on the shipped code path	BMC (CBMC/SAT)

What the Rocq proof is: a fully-Qed theorem (0 Admitted, no axioms — the file ends with Print Assumptions, and the compile log shows "Closed under the global context") about an abstract state machine that mirrors src/executor.rs field-by-field and operation-by-operation, with the correspondence documented inline. It quantifies over all finite interleavings of the modeled operations — something neither the per-function Verus contracts nor the bounded Kani harnesses state in that form. Gate: bazel test //proofs:executor_proofs_test (in the Formal Verification workflow).

What it is NOT: a proof about the compiled binary. There is no extraction, no refinement, and no translation-validation connecting the Rocq model to the Rust source or to the dissolved native artifact — the model-to-source correspondence is a structural argument (readable, but human-checked). The value of the Rocq track here is diverse redundancy: the same property formalized twice, independently, and checked by two engines with disjoint trusted bases (Z3's SMT core vs Rocq's kernel), plus a third bounded check on the executable path. A spec-encoding mistake or soundness bug in any single track alone can no longer silently invalidate the property.

Functional testing (CI-enforced on every commit):

• cargo test: runtime tests on stripped (non-Verus) code — current pass/fail via the Rust CI badge above (cargo test --workspace)
• Zephyr integration: the upstream kernel test suites on QEMU (M3 + MPS2/AN385 with MPU) — current pass/fail via the Zephyr Tests badge above
• Renode emulation: 3 boards (Cortex-M4F, M33, R5)
• Coverage: Rust + Zephyr C line coverage → Codecov

Honesty note: Formal verification requires Bazel + Nix and runs via the Formal Verification workflow (triggered on src/proofs/ffi changes + weekly cron). Functional tests run on every commit. See verification honesty assessment for the full gap analysis.

• Kani BMC: 185 bounded model checking harnesses (87 model + 98 FFI, Bazel-only)
• Differential testing: POSIX/FreeRTOS reference models validate spec independence
• Property-based testing: Proptest with random operation sequences
• Fuzz testing: Coverage-guided mutation via cargo-fuzz
• Miri: Undefined behavior detection

CI

3 workflows:

Workflow	Scope	Status
Rust CI	cargo test, clippy, verus-strip gate	see Rust CI badge above
Zephyr Kernel Tests	upstream kernel test suites on qemu_cortex_m3	see Zephyr Tests badge above
Renode Emulation Tests	Cortex-M4F (STM32F4) + Cortex-M33 (STM32L552) + Cortex-R5 (ZynqMP)	3 boards

Traceability

ASPICE V-model traceability managed by Rivet:

rivet validate # schema + traceability validation (the PASS gate)
rivet coverage # per-rule V-model coverage
rivet stats # artifact counts

Known Gaps

rivet validate surfaces lifecycle-coverage warnings (run it for the live count). The categories below explain what they are and why each is expected.

Expected -- KILN Phase 2 (8 warnings)

SWREQ-KILN-001 through 006 and SYSREQ-KILN-001/002 are draft requirements for the Kiln build-system integration phase. No implementation exists yet; these warnings are expected and will resolve when Phase 2 begins.

Lifecycle -- verification measures link to SWDD/SWARCH, not individual SWREQs (25 warnings + 277 gaps)

The remaining 25 warnings are system-level requirements (SYSREQ-*) for newer modules (fifo, lifo, queue, mempool, futex, timeout, poll, scheduler, timeslice, kheap, thread_lifecycle, heap, mem_domain, stack_config, device_init, fault_decode, ring_buf, userspace, work, fatal, dynamic, smp_state, atomic, mbox) that lack sys-verification and/or sys-integration-verification artifacts. This is a design choice: verification measures are linked at the SWDD and SWARCH levels, and roll up via traceability rather than duplicating at every requirement.

The 277 lifecycle gaps break down as:

• 243 SWREQ gaps: All missing unit-verification and sw-integration-verification direct links. These SWREQs are verified (97.6% swe1-has-verification coverage) but through SWDD-level verification measures, not direct SWREQ-to-test links.
• 34 SYSREQ gaps: 9 have only sys-integration-verification missing (sem, mutex, condvar, event, msgq, stack, pipe, mem_slab, timer -- the original 9 primitives with Zephyr tests). The other 25 are missing both sys-verification and sys-integration-verification (the newer Phase 2 modules).

Legitimate gaps: 0. All warnings are either expected (KILN Phase 2) or are a consequence of the lifecycle architecture where verification measures attach to design artifacts rather than being duplicated per-requirement.

Orphan artifacts: 2 (ZEP-SRS-5-3, PROV-SEM-002) -- known out-of-scope Zephyr upstream items.

Build

# Rust tests
cargo test# Verus verification
bazel test //:verus_test
# verus-strip gate (plain/ sync check)
cargo test --manifest-path tools/verus-strip/Cargo.toml --test gate
# Zephyr integration (requires west + Zephyr SDK)source .venv/bin/activate
export ZEPHYR_BASE=/path/to/zephyr
west build -b qemu_cortex_m3 zephyr/tests/kernel/semaphore/semaphore \
-- -DZEPHYR_EXTRA_MODULES=$(pwd) -DOVERLAY_CONFIG=$(pwd)/zephyr/gale_overlay.conf
west build -t run

License

Apache-2.0