Formally verified WebAssembly toolchain for safety-critical systems
Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals.
.wasm |
→ | Meld fuse |
→ | Loom optimize |
→ | Synth transpile |
→ | Kiln fire |
| sigil · attest · sign · verify | ||||||||
|
Statically fuses multiple WebAssembly components into a single core module. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time — runtime linking eliminated entirely. Every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness. |
Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through SMT translation validation and mechanized proofs. Includes a fused mode purpose-built for Meld output. |
|
Transpiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations for provably optimal native code. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation. Translation validation ensures the transpiled output faithfully preserves WebAssembly semantics. |
WebAssembly runtime for safety-critical systems. Full Component Model and WASI 0.2 support with a modular |
Sigil — Supply Chain Security
The cryptographic backbone of the pipeline. Every stage — fusion, optimization, compilation — creates a signed transformation attestation recording what changed, which tool version ran, and cryptographic hashes of inputs and outputs. The full chain is verifiable end-to-end.
Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool version and hash constraints. Hardware security via TPM 2.0. Offline verification for air-gapped embedded environments. IoT device provisioning with pre-provisioned trust bundles. All signatures embedded directly in WebAssembly modules — no external registry required.
Note
Correctness at every layer — Rocq mechanized proofs, Kani bounded model checking, Z3 SMT verification, and Verus Rust verification are used across the toolchain — not confined to individual projects. Sigil attestation chains bind it all together. No transformation ships without a proof.
Build & Verification
- rules_wasm_component — Bazel rules for WebAssembly Component Model across Rust, Go, C++, and JavaScript
- rules_rocq_rust — Bazel rules for Rocq theorem proving and Rust formal verification with hermetic Nix toolchains
- rules_verus — Bazel rules for Verus Rust verification
- rules_moonbit — Bazel rules for MoonBit with hermetic toolchain support
AI & MCP
Developer Tools
- thrum — Gate-based pipeline orchestrator for autonomous AI-driven development
- temper — GitHub App that hardens repositories to organizational standards
- wasm-component-examples — Working examples for Component Model development in C, C++, Go, and Rust
- moonbit_checksum_updater — Native MoonBit checksum management with GitHub API integration
Rust · WebAssembly Component Model · WASI 0.2 · 0.3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore