A WebAssembly Component Model toolchain for safety-critical systems, with formally verified components
Components are composed at build time and lowered to native code — the interface boundaries exist while you build and are gone when you ship.
components ──▶ meld ──▶ loom ──▶ synth ──▶ native
fuse optimize compile
kiln — interpret, on host or device
Everything the pipeline produces is signed and attested by sigil; everything it claims is traced by rivet.
| meld | Statically fuses WebAssembly components into one core module — import resolution, index-space merging, canonical-ABI adapter generation at build time, so nothing links at runtime. |
| loom | WebAssembly optimizer. Each rewrite is checked by SMT translation validation per run — a validated pass, not a verified tool. |
| synth | Transcodes WebAssembly to native ARM and RISC-V via program synthesis, targeting bare-metal Cortex-M/R. Declines an operation loudly rather than emitting code it cannot justify. |
| kiln | WebAssembly interpreter and runtime — full Component Model and WASI 0.2, with a no_std path for embedded. |
| sigil | Signing and attestation. Each stage records what changed, which tool version ran, and the hashes in and out; signatures embed in the module itself, and verification works offline for air-gapped devices. |
Different techniques, named separately — because they prove different things.
| rivet | Typed SDLC artifacts and traceability. Requirements, design, verification and their links as a checked graph; release readiness is a query over closed evidence rather than a date. |
| witness | MC/DC structural coverage measured on the lowered WebAssembly the runtime executes, not on the source it came from. |
| scry | Sound abstract interpretation — over-approximates, so it never misses a behaviour that can occur. Mechanized Rocq soundness proofs for specific domains. |
| ordeal | Certificate-checked QF_BV SMT. The solver is untrusted; an independent, formally-verified LRAT checker re-derives every UNSAT. |
| spar | Architecture models — AADL v2.3, SysML v2, CAN-DBC — with 30+ analyses including scheduling, fault trees and network-calculus timing bounds, and Lean proofs of the analyses themselves. |
| gale | Formally verified Rust replacements for Zephyr RTOS kernel primitives (Verus + Rocq + Lean), composing toward gust — an OS built from verified components. |
What "verified" means here. Verus (SMT, partial correctness, declared trusted base) · Kani (bounded model checking) · Rocq and Lean (specific theorems) · translation validation (per run, not the tool) · sound static analysis. Specific properties of specific components are proven. The toolchain as a whole is not, and we don't claim it is — see the preprint for where the gates are still weak.
| relay | Flight software as WebAssembly components, inspired by NASA's cFS. |
| wohl | OTA update and device lifecycle. |
| jess | Hardware integration — getting verified components onto real boards and into flight. |
Build & toolchain
- varve — pinned, signed, dated toolchain bundles; projects freeze on a layer and stay there (design)
- rules_wasm_component — Bazel rules for the Component Model across Rust, Go, C++, JavaScript
- rules_rocq_rust · rules_verus · rules_lean · rules_ordeal — hermetic Bazel rules for the proof and verification toolchains
- temper — GitHub App that holds repositories to organizational standards
Examples & utilities
- wasm-component-examples — Component Model examples in C, C++, Go, Rust
- bazel-file-ops-component — cross-platform file operations for Bazel, as a Wasm component
Rust · WebAssembly Component Model · WASI 0.2 · Bazel · Verus · Rocq · Lean · Kani · Sigstore
Everything is work in progress. Claims are scoped to what is checked.