I suggest you encoding your invariants in the harness. Architectural invariants that can be mechanically checked, including which modules are approved, which de

I suggest you encoding your invariants in the harness. Architectural invariants that can be mechanically checked, including which modules are approved, which dependencies, etc.