|
4 | 4 | (scope "formal verification and fuzzing") |
5 | 5 | (allow ("analysis" "fuzzing" "proof checks" "session type verification")) |
6 | 6 | (deny ("write to parser" "write to evaluator" "write to spec")) |
7 | | - (notes "May open findings on Harvard separation violations; code changes require explicit approval")) |
| 7 | + (notes "May open findings on Harvard separation violations; code changes require explicit approval") |
| 8 | + |
| 9 | + ;; Verification schedule and levels |
| 10 | + ;; 007 is a critical private repo — runs weekly at full level. |
| 11 | + ;; Currently Rust-based; Idris2 ABI layer planned but not yet present. |
| 12 | + ;; |
| 13 | + ;; Levels: |
| 14 | + ;; micro - panic-attack + A2ML manifest validation only (fast, local, every push) |
| 15 | + ;; standard - micro + Idris2 proof compilation + ABI contract checks (weekly) |
| 16 | + ;; full - standard + Z3 refinement + session type verification (monthly, via Groove) |
| 17 | + ;; attestation - full + Agda --cubical path types + signed certificate (on-demand, critical repos) |
| 18 | + ;; |
| 19 | + ;; Schedule options: "weekly" | "biweekly" | "monthly" | "on-push" | "on-demand" |
| 20 | + (verification |
| 21 | + (schedule "weekly") ;; Critical private repo — weekly deep checks |
| 22 | + (level "full") ;; Deep verification for agent meta-language |
| 23 | + |
| 24 | + ;; Individual check toggles |
| 25 | + ;; Checks are enabled/disabled based on 007's current implementation state. |
| 26 | + ;; Several checks are disabled pending the type checker build. |
| 27 | + (checks |
| 28 | + ;; --- micro level --- |
| 29 | + (panic-attack #t) ;; Surface vulnerability scan (local, fast) |
| 30 | + (a2ml-manifests #t) ;; Validate A2ML manifest structure and cross-references |
| 31 | + |
| 32 | + ;; --- standard level --- |
| 33 | + (abi-contracts #t) ;; Verify ABI definitions — will use Idris2 when ABI layer lands |
| 34 | + (idris2-proofs #f) ;; DISABLED: 007 is Rust, not Idris2 (enable when ABI layer is Idris2) |
| 35 | + (ffi-contracts #f) ;; DISABLED: no Zig FFI layer yet (enable with Idris2 ABI layer) |
| 36 | + (dependency-audit #t) ;; cargo-audit for Rust dependencies |
| 37 | + |
| 38 | + ;; --- full level --- |
| 39 | + ;; NOTE: refinement-smt and session-types will be enabled when the 007 |
| 40 | + ;; type checker is built. Session types are core to 007's choreography |
| 41 | + ;; system and will become a critical verification target. |
| 42 | + (refinement-smt #f) ;; DISABLED: not yet implemented — enable with type checker |
| 43 | + (session-types #f) ;; DISABLED: not yet implemented — enable with type checker |
| 44 | + |
| 45 | + ;; --- attestation level --- |
| 46 | + (cubical-paths #f)) ;; DISABLED: not yet implemented — enable with type checker |
| 47 | + |
| 48 | + ;; Groove endpoint for remote verification (full and attestation levels) |
| 49 | + (groove-endpoint "groove://localhost:9700/echidna") |
| 50 | + |
| 51 | + ;; Output location for signed verification certificates (attestation level) |
| 52 | + (attestation-output ".machine_readable/attestations/"))) |
0 commit comments