WebAssembly-to-native AOT compiler (ARM Cortex-M/R · RISC-V · AArch64) with mechanized correctness proofs
Badge numbers are machine-derived into artifacts/status.json and CI-staleness-gated — never hand-typed.
The coverage badge is Rust-test line coverage only — it cannot see the execution differentials, which run the compiler as a separate uninstrumented process from other CI jobs. It understates the testing that exists and is not a completeness measure; the differential population is counted separately in executed checks (#910).
Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, --target cortex-r5), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, -b aarch64). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon --relocatable cortex-m7dp VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residuals are f32.{ceil,floor,trunc,nearest}, which loud-decline on every ARM target pending a real VRINT.F32 lowering (v0.54 — the legacy pseudo-op was unsound via a saturating VCVT), and i64.trunc_sat_f32_* declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in Rocq cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs.
This is pre-release software. Generated code is validated by unit tests, Renode/QEMU emulation, execution differentials against wasmtime, and — for specific fixtures — cycle- and correctness-gated runs on real Cortex-M silicon (NUCLEO-G474RE, STM32F100, via the gale test loop). Broad hardware validation is still missing. Use at your own risk.
Part of PulseEngine -- a WebAssembly toolchain for safety-critical embedded systems:
| Project | Role |
|---|---|
| Synth | WASM-to-ARM AOT compiler with Rocq proofs |
| Loom | WASM optimizer with Z3 verification |
| Meld | WASM Component Model static fuser |
| Kiln | WASM runtime for safety-critical systems |
| Sigil | Supply chain attestation and signing |
Synth's pitch is that functional safety is a certification problem, not a processor problem: the right unit of evidence is verifiable code generation from a small, well-defined source language (WASM) to a small, well-defined target ISA (Thumb-2 / RV32), not a verified silicon core. Synth contributes the codegen half of that workflow: a compiler whose lowering steps come with mechanized proofs and an explicit Spectre / speculative-execution policy per lowering rule.
Requires Rust 1.88+ (edition 2024).
git clone https://github.com/pulseengine/synth.git
cd synth
cargo build --release -p synth-cliThe binary is at target/release/synth. Add it to your PATH or invoke directly.
Bazel 8.x builds Rust, Rocq proofs, and Renode emulation tests hermetically via Nix.
bazel build //crates:synth# Compile a WAT file to a Cortex-M ELF binary
synth compile examples/wat/simple_add.wat --cortex-m -o firmware.elf
# Disassemble the result
synth disasm firmware.elfTranslation validation (synth verify, --verify) is feature-gated in the CLI. Since v0.27.0 the default verification engine is ordeal, a pure-Rust QF_BV solver — synth-verify itself no longer needs a C++ toolchain. The CLI verify feature currently also enables the feature-gated Z3 differential oracle (statically linked):
cargo build --release -p synth-cli --features verify
synth verify examples/wat/simple_add.wat firmware.elf| Category | Status | Notes |
|---|---|---|
| i32 arithmetic, bitwise, comparison, shift/rotate | Tested | Full Rocq T1 proofs, Renode execution tests |
| i64 (register pairs): arithmetic, shifts, rotates, div/rem, compare | Tested | full pair lowering — right shifts fixed v0.28.0 (#599), rot/div/rem v0.30.1 (#610), A32 completeness v0.30.2 (#615); differential vs wasmtime |
| Scalar f32/f64 via VFP on FPU targets | Implemented | Complete f32 (v0.41) + f64 (v0.43, #369 closed) incl. AAPCS-VFP marshalling; execution differentials vs wasmtime; non-FPU targets loud-reject; residual: i64.trunc_sat_f32_* declines on single-precision FPUs (needs the f64 promote). The falcon --relocatable cortex-m7dp D-register-pressure + RA tail closed in v0.53 (#881); trunc_sat shipped v0.49 (#782) |
| WASM SIMD via ARM Helium MVE | Experimental | Cortex-M55 only; encoding untested on hardware |
| Control flow (block, loop, if/else, br, br_table) | Tested | Renode execution tests, complex test suite |
| Function calls (direct, indirect) | Implemented | call_indirect traps per WASM §4.4.8 (OOB index, type mismatch, null slot); self-contained --cortex-m dispatch via a PC-relative flash funcref table since v0.47 (#275), execution-differential-gated vs wasmtime |
| Memory (load/store, sub-word, size/grow) | Implemented | memory.grow returns -1 on embedded (fixed memory) |
| Globals, select | Implemented | R9-based globals; unit tests only |
| ELF output with vector table | Implemented | Thumb bit set on symbols; not linked on real hardware |
| Linker scripts (STM32, nRF52840, generic) | Implemented | Generated, not tested with real boards |
Cross-compilation (--link flag) |
Implemented | Requires arm-none-eabi-gcc in PATH; not CI-tested |
| Rocq mechanized proofs | CI-derived (badges above) | i32 + i64 T1 correctness proofs; the selector-DSL rule theorems are stated directly about the GENERATED model (VCR-ISA-001 #667 — rule_X := Gen.rule_X, single source VcrSelRulesGenerated.v); all four i32 div/rem trap guards discharged against the branch-taking executor (#73); counts re-derived into artifacts/status.json on every commit |
| SMT translation validation | ordeal (pure-Rust QF_BV) default | v0.27.0 (#553); Z3 demoted to feature-gated differential oracle — 141/141 agreement |
| WebAssembly spec test suite | CI-tracked compile rate | Compilation only — not executed on emulator |
- Narrow hardware coverage — silicon validation is fixture-scoped (gale's NUCLEO-G474RE / STM32F100 cycle and correctness gates); there is no broad board matrix
- Multi-memory is phase 1 — N memories lower to N distinct native base regions on ARM
--relocatable(v0.43, #749); fused-component paths beyond that still need single-memory mode - No WASI on embedded — kiln-builtins crate doesn't exist yet
- No component model execution — components compile but can't run without kiln-builtins;
cabi_reallocbinds natively (synthesized in-module arena allocator) on self-contained dissolves since v0.47 (#418 closed) - Spill-on-exhaustion is opt-in — Belady spilling is default-on (v0.24.0, VCR-RA-001), but replacing the register-exhaustion decline with allocation-time spilling (
SYNTH_SPILL_ON_EXHAUST, #580) is held for silicon numbers - No tail call optimization — return_call compiles but doesn't optimize the call frame
- SIMD/Helium is untested — MVE instruction encoding implemented but never run on M55 silicon or emulator
# Compile a WAT file to an ARM ELF binary
synth compile examples/wat/simple_add.wat -o add.elf
# Compile with a built-in demo (add, mul, calc, calc-ext)
synth compile --demo add -o demo.elf
# Compile a complete Cortex-M binary (vector table, startup code)
synth compile examples/wat/simple_add.wat --cortex-m -o firmware.elf
# Compile all exported functions
synth compile input.wat --all-exports -o multi.elf
# Compile and formally verify the translation
synth compile input.wat --verify -o verified.elfsynth disasm add.elf# Standalone verification: check that an ELF faithfully preserves WASM semantics
synth verify input.wat output.elfsynth backendsgraph LR
A["WAT / WASM"] --> B["Parse &<br/>Decode"]
B --> C["Instruction<br/>Selection"]
C --> D["Peephole<br/>Optimizer"]
D --> E["ARM<br/>Encoder"]
E --> F["ELF<br/>Builder"]
F --> G["ARM ELF<br/>Binary"]
style A fill:#654FF0,color:#fff
style G fill:#CE422B,color:#fff
Pipeline stages:
- Parse -- decode WASM binary or WAT text via
wasmparser/watcrates - Instruction selection -- pattern-match WASM ops to ARM instruction sequences (i32, i64, f32, f64, SIMD)
- Peephole optimization -- redundant-op elimination, NOP removal, instruction fusion, constant propagation (0-25% code reduction)
- ARM encoding -- emit 32-bit ARM / Thumb-2 machine code
- ELF builder -- produce ELF32 with
.text,.isr_vector,.data,.bss, symbol table; optional vector table and reset handler for Cortex-M
Per the PulseEngine Verification Guide, projects target multi-track verification. Current status:
| Track | Status | Coverage |
|---|---|---|
| Rocq | Partial | i32 + i64 T1 result-correspondence; float/SIMD T2; selector-DSL rule theorems stated directly about the GENERATED model (VCR-ISA-001 #667); all four i32 div/rem trap guards discharged (#73). Counts: artifacts/status.json (CI-re-derived; badges above) |
| Kani | Starting | Bounded model checking harnesses for the ARM encoder (count: artifacts/status.json) |
| Verus | Starting | Spec functions in synth-synthesis/src/contracts.rs; Bazel integration via rules_verus (count: artifacts/status.json) |
| Lean | Not started | — |
See artifacts/verification-gaps.yaml for the detailed gap analysis (VG-001 through VG-008).
Mechanized proofs in Rocq 9 show that compile_wasm_to_arm preserves WASM semantics for each operation. The proof suite lives in coq/Synth/ and covers ARM instruction semantics, WASM stack-machine semantics, and per-operation correctness theorems.
Qed/Admitted counts: artifacts/status.json — machine-derived and CI-gated
(claims.yaml + scripts/claim_check.py); surfaced by the badges at the top.
T1 result-correspondence (ARM output = WASM result): all i32 ops and all
i64 ops — i64 T1 parity since v0.11.0, 0 i64 admits (coq/STATUS.md)
T2 existence-only: f32/f64 and remaining categories
T3 admitted: 2 ArmRefinement.v
(0 division admits — all four i32 div/rem trap guards discharged against
exec_program_br, #73 closed at i32; #166 discharged the 2 Compilation.v
example admits via vm_compute; #933 closed the former CorrectnessSimple.v
i32_const_correct modeling-gap T3 by normalizing I32Const at the WASM
model boundary — the MOVW+MOVT reconstruction Qed now discharge it; the
2 ArmRefinement.v admits are opaque-sail_exec_instr-
axiom placeholders superseded by SailArmBridge.v)
incl. the selector-DSL rule theorems (Synth/VcrSelRules.v — every manifest
rule has a 1:1 Qed correctness theorem, count-same CI-gated against
coq/vcr_sel_rules.manifest) — stated directly about the GENERATED model
(VCR-ISA-001 #667: rule_X := Gen.rule_X, single source
Synth/VcrSelRulesGenerated.v emitted from the shipped sel_dsl::RULES, so
a selector-table change breaks the matching Qed), the VCR-SEL-001
pilot lemmas (Synth/VcrSelPilot.v, #386), and the Sail/ASL bridge
lemmas (ARM/SailArmBridge.v, VCR-ISA-001)
i32 and i64 operations have full T1 (result-correspondence) proofs; i64 parity landed in v0.11.0. The four i32 div/rem trap-guard proofs are discharged against the branch-taking executor exec_program_br (#73). The f32, f64, and SIMD instruction selection has T2 existence proofs but not T1 result-correspondence.
Build the proofs:
# Hermetic build via Bazel + Nix
bazel test //coq:verify_proofs
# Or locally with Rocq 9
cd coq && make proofsSee coq/STATUS.md for the per-file coverage matrix.
The synth-verify crate encodes WASM and ARM semantics as QF_BV formulas and checks per-rule equivalence. Since v0.27.0 (#553/#595) the default engine is ordeal, a pure-Rust QF_BV solver (139/139 validator tests, ~2 s; no C++ toolchain required); Z3 is demoted to a feature-gated (z3-solver) differential oracle — 141/141 cases, zero disagreements with ordeal. The --verify CLI flag invokes validation after compilation; synth verify provides standalone validation.
Replace synth's patch-accreting code generator with foundationally-verified, allocator-robust infrastructure — correctness from construction, not an ever-growing pile of locally-correct patches. In one sentence: moving from "we patched every bug we found" to "the structure makes the bug unrepresentable."
That is the means. The end it buys: match native code generation, and beat it where a verified compiler can do something an unverified one cannot.
Measured today (artifacts/parity-benchmark.md, regenerable): the default path
is 1.64×–3.48× larger than native C/Rust at -Os. Supplied with a proven
premise as a certificate, the same kernels reach 0.54× on the clamp shape —
below gcc -Os, within two bytes of the LLVM floor — and 1.00× on software
bounds, where the guarded build equals the unguarded one and the guard tax is
gone entirely.
LLVM cannot do the second. It cannot elide a check it cannot prove redundant, and it has no way to accept a proof from outside. That asymmetry is the programme: verification is not a tax paid for safety, it is the mechanism that lets this compiler go somewhere an unverified one cannot follow.
Cycles are not measured. Every cycles cell in the benchmark reads
OPEN — gale silicon (DWT). The size story is real; the speed story is
unproven, and this line stays until that changes.
Epic #242 is the source of truth — tracks, per-item status, done-criteria and the open gaps. This section is a pointer, on purpose: it used to restate the roadmap, and restating it is exactly how three of its status claims drifted out of date while the machine-derived badges above stayed correct.
| looking for | read |
|---|---|
| the roadmap and each item's status | epic #242 · artifacts/verified-codegen-roadmap.yaml |
| the numbers behind the claims above | artifacts/parity-benchmark.md |
| proof coverage, per file and tier | coq/STATUS.md |
| the exact op surface and every decline | docs/status/FEATURE_MATRIX.md |
| what shipped in which release | CHANGELOG.md |
| release scope as a live query | artifacts/release-v*.yaml (rivet release: + status:) |
| Crate | Purpose |
|---|---|
synth-cli |
CLI entry point (synth compile, synth verify, synth disasm) |
synth-core |
Shared types, error handling, Backend trait, WASM decoder |
synth-frontend |
WASM Component Model parser and validator |
synth-backend |
ARM Thumb-2 (Cortex-M) + A32 (Cortex-R5) encoder, ELF builder, vector table, linker scripts, MPU |
synth-backend-riscv |
RISC-V RV32IMAC backend (selector, encoder, relocatable ELF) — qemu_riscv32 / ESP32-C3 |
synth-backend-aarch64 |
AArch64 (A64) host-native backend, -b aarch64 — i32/i64 integer core, the complete scalar f32/f64 surface (v0.54), bounds-checked linear memory, globals, call_indirect with all three §4.4.8 trap guards, direct calls, and full control flow. See the feature matrix for the exact op surface and the mechanically-enumerated declines |
synth-backend-awsm |
aWsm backend integration (WASM-to-native via aWsm) |
synth-backend-wasker |
Wasker backend integration (WASM-to-Rust transpiler) |
synth-synthesis |
WASM-to-ARM instruction selection, peephole optimizer, pattern matcher |
synth-cfg |
Control flow graph construction and analysis |
synth-opt |
IR-level optimization passes (CSE, constant folding, DCE) |
synth-verify |
SMT translation validation — ordeal (pure-Rust QF_BV) default, Z3 feature-gated differential oracle |
synth-analysis |
SSA, control flow analysis, call graph |
synth-abi |
WebAssembly Component Model ABI (lift/lower) |
synth-memory |
Portable memory abstraction (Zephyr, Linux, bare-metal) |
synth-qemu |
QEMU integration for testing |
synth-test |
WAST-to-Robot Framework test generator for Renode |
synth-wit |
WIT (WebAssembly Interface Types) parser |
# Run all Rust tests
cargo test --workspace
# Lint
cargo clippy --workspace --all-targets -- -D warnings
cargo fmt --check
# Bazel: Rocq proofs + Renode ARM Cortex-M4 emulation tests
bazel test //coq:verify_proofs
bazel test //tests/...- Architecture -- compilation pipeline, components, binary emission
- Synth & Loom -- two-tier architecture
- Feature Matrix -- what works, what doesn't (generated; numbers from
artifacts/status.json) - Status (machine-derived) -- CI-re-derived counts: proofs, verified rules, backend coverage
- Requirements -- functional and non-functional requirements
- Research -- literature review, formal methods, Sail/ARM analysis
- Roadmap -- the VCR-* program (single source of truth for roadmap status; see also the North Star section and Changelog)
- Contributing -- how to contribute
Apache-2.0 -- see LICENSE.
Part of PulseEngine — WebAssembly toolchain for safety-critical systems