Skip to content

Add GitHub Actions CI surfacing existing Bazel + Kani + proptest + sanitizer verification #21

@avrabe

Description

@avrabe

Part of the V&V coverage initiative.

Problem

gale runs extensive verification today — 27 Bazel test targets, 1,100+ Kani uses, 20+ integration tests, 24 proptest modules, 16 cargo-fuzz targets, ASAN/TSAN/LSAN wired in .cargo/config.toml, Zephyr test suites on emulated Cortex-M3/M4F/M33/R5 — but there is no .github/workflows/ directory. All verification is invisible from GitHub, which hurts the certification-artifact story.

Acceptance

  • Create .github/workflows/ci.yml that runs on PR + main push:
    • bazel test //... on Linux x86_64 + macOS aarch64
    • Kani verification matrix (cargo kani on the primitives that have harnesses)
    • proptest suite
    • Sanitizer matrix: RUSTFLAGS="-Zsanitizer=address", thread, leak with cargo +nightly test
    • cargo-fuzz smoke (short budget, e.g. 60s per target)
  • Create .github/workflows/nightly.yml for longer-running jobs:
    • Extended Kani bounds
    • cargo-fuzz long runs (1h per target)
    • Zephyr QEMU test matrix (cortex_m3/m4f/m33/r5)
  • Status badges added to README
  • Per-job artifacts uploaded for audit (Kani reports, sanitizer logs, fuzz corpus)

Notes

  • Zephyr tests may need west tooling + QEMU setup — follow Zephyr's standard CI pattern
  • Keep Bazel as the hermetic gate; GH Actions just invokes it
  • Sanitizer runs require nightly Rust — use the pin in z/gale/rust-toolchain.toml note header

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions