docs: book chapters 13-16 (formal verification, state safety, MLOps, agents) by noahgift · Pull Request #22 · paiml/forjar

noahgift · 2026-03-04T09:14:09Z

Summary

Chapter 13: Formal Verification & Provability (Kani, TLA+, SAT, Alloy, MC/DC, Verus, DO-330, flight-grade, Ferrocene, reproducible builds)
Chapter 14: State Safety & Disaster Recovery (saga pattern, generational snapshots, reversibility, integrity, staleness, event-sourced reconstruction)
Chapter 15: DataOps & MLOps Pipelines (data sources, validation, GPU management, model resources, training reproducibility, pipeline DAG)
Chapter 16: Agent Infrastructure & pforge (MCP servers, agent deployment, tool permissions, health monitoring, SBOM, recipe registry)
Updated SUMMARY.md with all new chapters

Test plan

All chapters reference actual source modules
YAML examples are valid forjar config syntax
SUMMARY.md includes all 16 chapters

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…→2396) - validate --check-resource-dependencies-complete (FJ-821): dep target existence - status --machine-resource-health (FJ-822): per-machine health breakdown - graph --resource-dependency-chain (FJ-823): full chain from root to leaf - apply --notify-teams-webhook (FJ-824): MS Teams adaptive card notifications - validate --check-machine-connectivity (FJ-825): address format validation - status --fleet-convergence-trend (FJ-826): convergence % across fleet - graph --bottleneck-resources (FJ-827): high fan-in + fan-out detection - status --resource-state-distribution (FJ-828): state counts across fleet Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…al paths (2396→2419) Validate: --check-resource-naming-pattern, --check-resource-provider-support Status: --machine-apply-count, --fleet-apply-history, --resource-hash-changes Graph: --critical-dependency-path, --resource-depth-histogram Apply: --notify-slack-blocks Split graph_advanced.rs → graph_paths.rs (FJ-823/827/831/835) to stay under 500-line limit. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…nce times (2419→2442) Validate: --check-resource-secret-refs, --check-resource-idempotency-hints Status: --machine-uptime-estimate, --fleet-resource-type-breakdown, --resource-convergence-time Graph: --resource-coupling-score, --resource-change-frequency Apply: --notify-custom-template New status_insights.rs module. Split try_status_phase68 + try_status_phase71 helpers. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

8 tickets: validate --check-resource-dependency-depth, --check-resource-machine-affinity, status --machine-drift-age, --fleet-failed-resources, --resource-dependency-health, graph --resource-impact-score, --resource-stability-score, apply --notify-custom-webhook. Split validate_advanced→validate_governance (500-line limit). Extract try_graph_paths helper (cognitive complexity). 2442→2463 tests. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

8 tickets: validate --check-resource-drift-risk, --check-resource-tag-coverage, status --machine-resource-age-distribution, --fleet-convergence-velocity, --resource-failure-correlation, graph --resource-dependency-fanout, --resource-dependency-weight, apply --notify-custom-headers. Extract try_validate_governance helper. 2463→2484 tests. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Implement 8 resource lifecycle & operational intelligence commands: - FJ-861: validate --check-resource-lifecycle-hooks - FJ-862: status --machine-resource-churn-rate - FJ-863: graph --resource-dependency-bottleneck - FJ-864: apply --notify-custom-json - FJ-865: validate --check-resource-provider-version - FJ-866: status --fleet-resource-staleness - FJ-867: graph --resource-type-clustering - FJ-868: status --machine-convergence-trend Split graph_paths→graph_scoring, status_insights→status_predictive. 2507 tests pass, all commands dogfooded. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Implement 8 capacity planning & configuration analytics commands: - FJ-869: validate --check-resource-naming-convention - FJ-870: status --machine-capacity-utilization - FJ-871: graph --resource-dependency-cycle-risk - FJ-872: apply --notify-custom-filter - FJ-873: validate --check-resource-idempotency - FJ-874: status --fleet-configuration-entropy - FJ-875: graph --resource-impact-radius - FJ-876: status --machine-resource-freshness Extract try_status_phase73, collect_type_entropy, flatten find_cycle_risks. 2530 tests pass, all commands dogfooded. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Phase 77 — Operational Maturity & Compliance Automation: - FJ-877: validate --check-resource-documentation - FJ-878: status --machine-error-budget - FJ-879: graph --resource-dependency-health-map - FJ-880: apply --notify-custom-retry - FJ-881: validate --check-resource-ownership - FJ-882: status --fleet-compliance-score - FJ-883: graph --resource-change-propagation - FJ-884: status --machine-mean-time-to-recovery 2553 tests pass. All commands dogfooded. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Phase 78 — Automation Intelligence & Fleet Optimization: - FJ-885: validate --check-resource-secret-exposure - FJ-886: status --machine-resource-dependency-health - FJ-887: graph --resource-dependency-depth-analysis - FJ-888: apply --notify-custom-transform - FJ-889: validate --check-resource-tag-standards - FJ-890: status --fleet-resource-type-health - FJ-891: graph --resource-dependency-fan-analysis - FJ-892: status --machine-resource-convergence-rate 2576 tests passing. Extracted validate_ownership.rs module. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Phase 79 — Security Hardening & Operational Insights: - FJ-893: validate --check-resource-privilege-escalation - FJ-894: status --machine-resource-failure-correlation - FJ-895: graph --resource-dependency-isolation-score - FJ-896: apply --notify-custom-batch - FJ-897: validate --check-resource-update-safety - FJ-898: status --fleet-resource-age-distribution - FJ-899: graph --resource-dependency-stability-score - FJ-900: status --machine-resource-rollback-readiness 2599 tests passing. Milestone: FJ-900 reached. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Phase 80 — Operational Resilience & Configuration Intelligence: - FJ-901: validate --check-resource-cross-machine-consistency - FJ-902: status --machine-resource-health-trend - FJ-903: graph --resource-dependency-critical-path-length - FJ-904: apply --notify-custom-deduplicate - FJ-905: validate --check-resource-version-pinning - FJ-906: status --fleet-resource-drift-velocity - FJ-907: graph --resource-dependency-redundancy-score - FJ-908: status --machine-resource-apply-success-trend 2622 tests passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Predictive Infrastructure Intelligence: dependency completeness validation, MTTR estimation, centrality scoring, state coverage, convergence forecasting, bridge detection, error budget forecasting, custom throttle notifications. 2645 tests passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Infrastructure Insight & Configuration Maturity: rollback safety validation, dependency lag detection, clustering coefficient, custom aggregate notifications, config maturity scoring, fleet dependency lag, modularity scoring, config drift rate. 2668 tests passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Phase 84: validate naming-standards + dependency-symmetry, status convergence-velocity + fleet-velocity + failure-recurrence, graph dependency-density + transitivity, apply notify-custom-routing. 2714 tests passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Phase 85: validate circular-alias + dependency-depth-limit, status drift-frequency + fleet-drift-frequency + apply-duration-trend, graph fan-out + fan-in, apply notify-custom-dedup-window. 2735 tests passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Split status_intelligence.rs and graph_intelligence.rs into _ext modules. Extracted dispatch_status_ext.rs for legacy phase routing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Automated cargo fix removed ~466 unused imports across 77 files. Manual fixes: too_many_arguments allow attrs, type_complexity allows, lifetime elision, needless_borrow, sort_by_key, length_comparison, map_or→is_some_and, match→if-let, identical if blocks, loop indexing. Restored cfg(test)-gated re-export for validate_int. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

FJ-957: validate --check-resource-content-hash-consistency FJ-958: status --machine-resource-drift-age FJ-959: graph --resource-dependency-longest-path (DAG critical chain) FJ-960: apply --notify-custom-backoff (exponential retry) FJ-961: validate --check-resource-dependency-refs FJ-962: status --fleet-resource-drift-age FJ-963: graph --resource-dependency-strongly-connected (Tarjan SCC) FJ-964: status --machine-resource-recovery-rate 22 new tests (2754→2776), dogfood example, book chapter updates. Split dispatch_notify.rs into dispatch_notify_custom.rs (file health). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…-965→FJ-972) 8 tickets: validate trigger-refs/param-type-safety, status drift-velocity/ fleet-recovery-rate/convergence-efficiency, graph topological-depth/weak-links, apply notify-custom-circuit-breaker. 2776→2799 tests, all passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…973→FJ-980) 8 tickets: validate env-consistency/secret-rotation, status apply-frequency/ fleet-health-score/staleness-index, graph minimum-cut/dominator-tree, apply notify-custom-dead-letter. 2799→2822 tests, all passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…J-988) 8 new commands: validate lifecycle-completeness/provider-compatibility, status drift-recurrence/drift-heatmap/convergence-trend-p90, graph resilience-score/pagerank, apply notify-custom-escalation. 2845 tests pass. New modules: graph_intelligence_ext2, status_intelligence_ext2. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

8 new commands: validate naming-convention-strict/idempotency-annotations, status drift-age-hours/convergence-percentile/error-rate, graph betweenness-centrality/closure-size, apply notify-custom-correlation. 2868 tests pass. New module: validate_ordering_ext. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…-1004) 8 new commands: validate content-size-limit/dependency-fan-limit, status convergence-gap/error-distribution/convergence-stability, graph eccentricity-map/diameter-path, apply notify-custom-sampling. 2891 tests pass. Refactored dispatch_status_cmd to reduce complexity. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…s PMAT-038) Add three new CLI commands: - `forjar bundle` — self-contained recipe bundles with BLAKE3 manifest (#92) - `forjar model-card` — ML model card generation (#152) - `forjar agent-sbom` — agent-specific bill of materials (#162) Score: 124 -> 127/166. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

… (Refs PMAT-038) - forjar repro-proof: BLAKE3 reproducibility certificate (config + git SHA + store + state) - forjar bundle --verify: re-hash all files for air-gap integrity verification - Split dispatch_misc_cmd to reduce cognitive complexity - Scorecard 127→130/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…, dataset lineage (Refs PMAT-039) - forjar data-freshness: mtime + BLAKE3 artifact freshness with --max-age SLA - forjar data-validate: source/artifact existence + integrity + store checks - forjar checkpoint: ML checkpoint listing, --gc --keep N garbage collection - forjar dataset-lineage: Merkle-hashed data pipeline lineage graph - Split dispatch_misc_cmd further to keep cognitive complexity <25 - Scorecard 130→136/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…eval (Refs PMAT-039) - forjar sovereignty: jurisdiction/classification/residency compliance audit - forjar cost-estimate: static resource cost + time analysis by type - forjar model-eval: ML evaluation pipeline with completion_check + artifact gating - Scorecard 136→139/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…s PMAT-039) - pforge-mcp-server.yaml: 4-phase MCP server deployment (#155) - agent-deployment.yaml: composable GPU+model+config+MCP+health (#156) - multi-agent-fleet.yaml: 3-machine fleet with LB + tool policies (#157,#158,#160,#161) - Scorecard 139→145/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…s, ISO export, brownfield import, cross-machine deps (Refs PMAT-039) - FJ-1420 (#76): forjar fault-inject — fault scenario generation per resource - FJ-1421 (#78): forjar invariants — runtime invariant monitors from policies - FJ-1422 (#91): forjar iso-export — offline deployment bundles with BLAKE3 manifest - FJ-1423 (#25): forjar import-brownfield — scan dpkg/systemd/config for state import - FJ-1424 (#11): forjar cross-deps — cross-machine dependency analysis + execution waves - 33 new tests (7448 total), spec scorecard 145→150/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ulti-config, stack graph (Refs PMAT-039) - FJ-1425 (#24): forjar state-backend — pluggable state backend trait + local impl - FJ-1426 (#66): forjar registry-list — versioned recipe registry with BLAKE3 - FJ-1427 (#69): forjar catalog-list — service catalog with parameterized blueprints - FJ-1428 (#118): forjar multi-apply — multi-config apply ordering via data source deps - FJ-1429 (#119): forjar stack-graph — stack dependency DAG with cycle detection - 31 new tests (7479 total), spec scorecard 150→155/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…vation, parallel stacks (Refs PMAT-039) - FJ-1430 (#27): forjar query — composable infrastructure search with filters - FJ-1431 (#28): forjar query --live — live SSH-based infrastructure probing - FJ-1432 (#31): forjar sign — BLAKE3-HMAC recipe signing with tamper detection - FJ-1433 (#34): forjar sign --pq — dual classical + post-quantum signing - FJ-1434 (#47): forjar preservation — pairwise resource preservation checking - FJ-1435 (#125): forjar parallel-apply — parallel multi-stack execution waves - 29 new tests (7508 total), spec scorecard 155→161/166 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…efs PMAT-039) - saga_coordinator.rs: SagaStep/SagaStepStatus types, compensating snapshots, cmd_saga_plan with directory-copy rollback; 5 tests - agent_registry.rs: AgentRecipe/AgentCategory types, versioned JSON registry, search by name/description/tags, cmd_agent_registry; 6 tests - dispatch_platform.rs: dispatch_agent_registry function - Spec scorecard: 145/166 implemented (87%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

… (Refs PMAT-039) - pull_agent.rs: ExecMode::Push (one-shot) / ExecMode::Pull (daemon loop) with configurable interval, drift detection via lock file comparison, auto-apply on drift, max_iterations; `forjar agent [--pull]` CLI - 12 tests covering both modes, drift detection, serde roundtrips - Spec scorecard: 147/166 implemented (89%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…PMAT-039) - kani_proofs.rs: 6 #[kani::proof] harnesses — BLAKE3 idempotency, collision resistance, converged-is-noop, status monotonicity, plan determinism, topo sort stability; 6 runtime unit tests - ForjarExecution.tla: TLA+ spec with Init/Next/Fairness; safety (dependency order, no regression), liveness (convergence, termination), idempotency properties; parameterized over RESOURCES/DEPENDENCIES - Spec scorecard: 149/166 implemented (90%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

… PMAT-039) - planner/sat_deps.rs: DPLL SAT solver with unit propagation; dependency constraints as CNF clauses; Satisfiable/Unsatisfiable result with conflict diagnosis; 6 tests - ForjarDependencyGraph.als: Alloy spec with Resource/Machine/Position sigs; no_cycles/unique_names facts; transitive_order/complete_coverage assertions; linear_chain/diamond/independent predicates - Spec scorecard: 151/166 implemented (91%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…#43, #44, #46) (Refs PMAT-039) - types/refinement.rs: Port, FileMode, SemVer, Hostname, AbsPath, ResourceName refinement types with compile-time const assertions; 13 tests - verus_spec.rs: observe/diff/apply/reconcile model with #[cfg(verus)] proofs for termination, convergence, idempotency, monotonicity; 8 tests - planner/minimal_changeset.rs: hash-based + dependency propagation minimal change set with provably minimal guarantee; 7 tests - Spec scorecard: 154/166 implemented (93%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…104) (Refs PMAT-039) - core/mcdc.rs: MC/DC test pair generation for AND/OR decisions; generate_mcdc_and/or produce independence pairs per DO-178C DAL-A; McdcReport with coverage_achievable flag; 8 tests - cli/structured_log.rs: Level enum with atomic global filter; JSON + human-readable output modes; log_event() with structured fields; Span with RAII enter/exit; 8 tests - Spec scorecard: 156/166 implemented (94%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

) (Refs PMAT-039) - cli/progress.rs: Spinner (10-frame animation, elapsed time); ProgressBar (ASCII bar, percentage, ETA estimation); ProgressTracker (multi-resource tracking); no deps; 11 tests - core/do330.rs: ToolQualLevel (TQL-1..5); Requirement traceability; CoverageEvidence (line/branch/MC-DC); QualificationPackage; 6 tests - Spec scorecard: 158/166 implemented (95%) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…#115) (Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…(Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ps, agents) (Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

… handlers, rollback-on-failure - generation.rs: Nix-style numbered state generations with atomic symlink swap - create_generation(), rollback_to_generation(), gc_generations(), list_generations() - forjar generation list/gc CLI commands; forjar rollback --generation N - Auto-generation creation during apply; 11 tests - compliance.rs: Structured compliance benchmark evaluation framework - CIS (6.1.1, 1.1.5, 5.2.1, 6.2.1), NIST 800-53 (AC-3, AC-6, CM-6, SC-28, SI-7) - SOC2 (CC6.1, CC7.2), HIPAA (164.312a, 164.312e); 22 tests - tests_proptest_handlers.rs: 6 property-based tests with arb_resource() strategy - Hash determinism, type-affects-hash, converged=noop, codegen no-panic - Proof obligation totality, chain hash determinism; covers 8 resource types - apply.rs: Generation-based rollback on failure via maybe_rollback_generation() - Fix: gc_old_snapshots() now uses snapshots_dir() consistently (was .snapshots) Score: 98 → 102/166 (#22 ⚠→✅, #75 ⚠→✅, #77 ⚠→✅, #83 ⚠→✅, #126 ❌→✅) (Refs PMAT-037) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

noahgift and others added 30 commits February 28, 2026 02:29

docs: Mark Phase 69 Done, define Phase 70 (FJ-821→FJ-828), update book

6d02e59

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

docs: Mark Phase 70 Done, define Phase 71 (FJ-829→FJ-836), update book

122fb81

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

docs: Phase 71 Done, define Phase 72, book examples (FJ-829→FJ-836)

26a2967

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

docs: Phase 72 Done, define Phase 73, book examples (FJ-837→FJ-844)

b2b217b

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

docs: Phase 73 Done (FJ-845→FJ-852), define Phase 74, book examples

a977ccd

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

docs: Phase 74 Done (FJ-853→FJ-860), define Phase 75, book examples

a13cdcb

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat: Phase 83 Done (FJ-925→FJ-932), define Phase 84, book examples

636c7aa

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat: Phase 86 Done (FJ-949→FJ-956), define Phase 87, book examples

bec242c

Split status_intelligence.rs and graph_intelligence.rs into _ext modules. Extracted dispatch_status_ext.rs for legacy phase routing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

noahgift and others added 19 commits March 4, 2026 00:37

feat: FJ-107+115: Interactive TUI mode + flight-grade execution (#107, …

61ea2bf

…#115) (Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat: FJ-110+113: LSP server + Ferrocene certification (#110, #113) (…

77e7d19

…Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat: FJ-095: Reproducible binary builds — 163/163 features complete …

fdca655

…(Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

docs: add book chapters 13-16 (formal verification, state safety, MLO…

35adf49

…ps, agents) (Refs PMAT-039) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

noahgift force-pushed the main branch from 3ed272c to e707e73 Compare March 20, 2026 14:34

noahgift force-pushed the main branch 3 times, most recently from 8cf6817 to f100dab Compare March 21, 2026 18:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

docs: book chapters 13-16 (formal verification, state safety, MLOps, agents)#22

docs: book chapters 13-16 (formal verification, state safety, MLOps, agents)#22
noahgift wants to merge 334 commits intomainfrom
batch-15-book-chapters

noahgift commented Mar 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

noahgift commented Mar 4, 2026

Summary

Test plan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant