-
Verify — three independent proof paths across everything
-
Verus proves Rust code via SMT/Z3 — preconditions, postconditions, invariants on every public function. Rocq machine-checks abstract invariants that hold regardless of implementation. Lean 4 proves scheduling theory — priority inheritance, deadline guarantees, starvation freedom.
-
These are not limited to one tool. Every component in the ecosystem — meld, loom, synth, kiln, gale, relay, wohl — carries formal verification. Three independent paths run in CI on every commit.
+
Verify — three proof paths and the empirical coverage cell
+
Verus proves Rust code via SMT/Z3 — preconditions, postconditions, invariants on every public function. Rocq machine-checks abstract invariants that hold regardless of implementation. Lean 4 proves scheduling theory — priority inheritance, deadline guarantees, starvation freedom. witness measures branch / MC/DC coverage at the post-compile WebAssembly level — the empirical counterpart that closes the §FM.6.7(f) / structural-coverage cell DO-178C, ISO 26262 Part 6 Table 12, and IEC 61508 Annex C expect.
+
These are not limited to one tool. Every component in the ecosystem — meld, loom, synth, kiln, gale, relay, wohl — carries formal verification. Four independent verification paths run in CI on every commit: three proof, one coverage.