chore: workspace cfg(kani) lint config + v1.0 rollout audit

Cargo.toml

@@ -51,6 +51,15 @@ rust-version = "1.85.0"
 wit-bindgen = { version = "0.57.1", default-features = false }
 proptest = "1"
 
+# Workspace-wide lint config. Engines use `#[cfg(kani)]` for the Kani
+# model-checker harness paths (they're built only under `cargo kani`,
+# which sets the `kani` cfg). Stable rustc sees the cfg as unexpected
+# and warns by default — declare it here so all member crates inherit
+# the check-cfg whitelist without per-crate boilerplate. Member crates
+# pick this up via `[lints] workspace = true` in their own Cargo.toml.
+[workspace.lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
 # All guest components are no_std + no alloc.
 # Memory comes from Kiln's capability-based allocator (safe_managed_alloc!)
 # or from Gale's mem_slab / heap on embedded targets.

artifacts/features/FEAT-FALCON-rollout.yaml

@@ -1591,9 +1591,11 @@ artifacts:
     status: pending
     description: >
       Full overdo matrix green across all six safety domains in
-      rivet validate output. Check-It checkers qualified for the
-      EKF and mixer (DO-330 path). falcon-coax and falcon-hex
-      variants ship alongside falcon-quad.
+      rivet validate output. Tool-qualification records (v0.14.3
+      pattern) extended to DO-330-grade per tool. falcon-coax and
+      falcon-hex airframe variants ship alongside falcon-quad.
+      All bench-evidence artifacts (PX4-SITL + gz-sim) carry
+      reproducible setup recipes + signed manifests.
 
       Ships:
         - DO-178C DAL-A credit bundle
@@ -1604,7 +1606,9 @@ artifacts:
         - EN 50128 SIL-4 credit bundle
         - falcon-coax world spec (Ingenuity-class)
         - falcon-hex world spec (fault-tolerant)
-        - Check-It qualified checkers for EKF + mixer
+        - DO-330-grade tool qualification reports for Verus / Kani
+          / miri / witness / spar (extends v0.14.3's auditable
+          starting-point TQ docs).
 
       v1.0 is when the evidence dossier clears the bar — not when
       the features are complete. v2.x adds falcon-vtol and

crates/relay-ccsds/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-cfdp/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-ci/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-cs/Cargo.toml

@@ -17,3 +17,6 @@ wit-bindgen = { workspace = true, default-features = false }
 
 # no_std + no alloc: WASM components run in bounded memory.
 # All allocation through Kiln capability system or static buffers.
+
+[lints]
+workspace = true

crates/relay-ds/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-fm/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-hk/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-hs/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-lc/Cargo.toml

@@ -22,3 +22,6 @@ relay-primitives = { path = "../relay-primitives" }
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true

crates/relay-md/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-mm/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-nid/Cargo.toml

@@ -23,3 +23,6 @@ crate-type = ["rlib"]
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true

crates/relay-sc/Cargo.toml

@@ -17,3 +17,6 @@ wit-bindgen = { workspace = true, default-features = false }
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true

crates/relay-sca/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-sch/Cargo.toml

@@ -20,3 +20,6 @@ wit-bindgen = { workspace = true, default-features = false }
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true

crates/relay-tbl/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

crates/relay-to/Cargo.toml

@@ -14,3 +14,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 wit-bindgen = { workspace = true, default-features = false }
+
+[lints]
+workspace = true

host/witness-wasi-harness/Cargo.toml

@@ -12,7 +12,7 @@ name = "witness-wasi-harness"
 path = "src/main.rs"
 
 [dependencies]
-wasmtime = "27"
+wasmtime = "45"
 wasmtime-wasi = "45"
 anyhow = "1"
 serde_json = "1"

host/witness-wasi-harness/src/main.rs

@@ -27,7 +27,11 @@ use std::env;
 use std::fs;
 use std::path::PathBuf;
 use wasmtime::{Config, Engine, Linker, Module, Store, Val};
-use wasmtime_wasi::preview1::{self, WasiP1Ctx};
+// wasmtime-wasi 44 renamed `preview1` → `p1`; bound here as `preview1`
+// so the rest of the file keeps reading naturally. PR #44 (Dependabot
+// 27→45 upgrade) merged with main still importing the old path; v0.19.2
+// catches it up.
+use wasmtime_wasi::p1::{self as preview1, WasiP1Ctx};
 use wasmtime_wasi::WasiCtxBuilder;
 
 /// `witness-harness-v1` schema — keys are decimal branch IDs as