Add Bazel sandbox support and improve production readiness #5
Description
Current state
rules_verus is very early (initial implementation). Bazel sandbox support is not yet implemented, which means builds are not hermetic and verification results may not be reproducible across environments.
Scope
- Add Bazel sandbox support for Verus compilation and verification
- Ensure Verus toolchain is fetched hermetically (consider Nix flake — see Add Nix flake for reproducible development and build environment #4)
- Add CI testing
- Document integration with rules_rust for verified Rust crate development
- Test with real verification targets (kiln interpreter, meld fusion logic)
Context
rules_verus is a key part of the PulseEngine verification story — it brings SMT-based Rust verification into the build system. For the pipeline's qualification goals, verification must be reproducible and hermetic, which requires sandbox support.
Related: rules_rocq_rust already has working Nix integration and can serve as a reference for hermetic toolchain provisioning.