Compliance as a
Mathematical Proof

Traditional FedRAMP authorization packages rely on prose-based System Security Plans, manually authored assessment reports, and periodic human review cycles. This approach introduces ambiguity, assessment latency, and a structural gap between an organization's stated controls and its operational reality.

The FedCloud Formal Verification Gateway (FVG) closes that gap entirely. Rather than describing security posture in natural language, the gateway encodes every material security invariant as a formal theorem in the Lean 4 interactive theorem prover. Live infrastructure state is ingested, translated into Lean's type system, and evaluated against those theorems. The result is a cryptographically-identified proof obligation — either satisfied or falsified — generated continuously and stored in an OSCAL-conformant repository.

6-Stage Architecture

Infrastructure telemetry flows left to right through six deterministic stages before producing an authorization-grade artifact.

Stage 1 — State Ingestion

The ingestion subsystem is a collection of typed adapters, one per telemetry source. Each adapter polls its source on a configurable interval (default: 5 minutes for configuration state, 1 minute for access events) and emits a state snapshot — a JSON document containing the full, current configuration of all in-scope resources plus a SHA-256 hash of the previous snapshot for chain linkage.

Supported telemetry sources in the current release include:

• Kubernetes API Server — Pod specs, RBAC bindings, NetworkPolicies, admission webhook configurations
• AWS Config — IAM policy documents, S3 bucket configurations, KMS key metadata, VPC ACLs
• AWS CloudTrail — API call records, authentication events, cross-account assumption logs
• IAM Access Analyzer — External access findings, policy analysis results
• Amazon CloudWatch / VPC Flow Logs — Network reachability, anomaly signals

Stage 2 — Translation to Lean 4 Types

The lean-bridge Python module reads each state snapshot and emits a .lean source file containing Lean 4 inductive type instances that faithfully represent the infrastructure state. The type definitions live in lean/FedCloud/Types.lean and are the canonical data contract between the Python pipeline and the theorem library.

Stage 3 — Lean 4 Kernel Evaluation

The pipeline invokes the Lean 4 compiler (lake build) against the generated state file. The kernel evaluates every theorem in lean/FedCloud/Invariants.lean by attempting to construct a proof term for each theorem with the current state substituted as the concrete value. This is not symbolic execution — it is full kernel-level type-checking with Lean's definitional equality.

Lean's trusted code base (TCB) consists of fewer than 10,000 lines of C++, independently reviewed, and conforms to the Calculus of Inductive Constructions (CIC). The kernel's correctness guarantee is foundational: a proof accepted by the kernel is equivalent to a formal mathematical proof under CIC semantics.

Stage 4 — Verification Output

The pipeline parses the Lean compiler's exit code and structured output to produce a Verification Receipt for each theorem. On failure, Lean's elaboration trace is parsed to identify the first term that failed to type-check, producing a structured counter-example pinpointing the non-compliant resource, attribute, and deviation.

Stage 5 — OSCAL Repository

The OSCAL writer consumes verification receipts and updates three artifact files in a dedicated Git repository. Each commit is signed with a hardware-backed key and references the state hash and theorem IDs covered by that evaluation run, creating an immutable, auditable chain of authorization evidence.

Stage 6 — Continuous Authorization

The authorization dashboard polls the OSCAL repository and renders a real-time control-family heatmap. When a theorem transitions from PASS to FAIL, the system automatically generates a draft POA&M entry, notifies the system owner via webhook, and logs the event to CloudTrail with finding severity classification aligned to CVSS v4.

The gateway organizes its security invariants into four clusters aligned to NIST SP 800-53 control families. Each cluster contains one or more Lean 4 theorems that must hold simultaneously for the cluster's authorization status to be PASS. A single failing theorem within a cluster causes the entire cluster to report FAIL to the authorizing official.

-- AC-6 Least Privilege / IA-2(6) Phishing-Resistant MFA
-- Every active privileged session must carry phishing-resistant MFA
-- and operate under a token lifetime not exceeding 60 minutes.
theorem identity_least_privilege_invariant (ctx : SecurityContext) :
  (∀ s ∈ ctx.active_sessions, s.is_privileged = true →
    (s.has_phishing_resistant_mfa = true ∧ s.token_lifetime_minutes ≤ 60)) → True

-- SC-28 Protection of Information at Rest
-- All deployed stores that contain federal data must be encrypted
-- at rest using a FIPS-140-3 validated cryptographic module.
theorem cryptographic_protection_invariant (state : InfrastructureState) :
  (∀ d ∈ state.deployed_stores, d.contains_federal_data = true →
    (d.is_encrypted_at_rest = true ∧ d.cryptographic_module_standard = "FIPS-140-3")) → True

-- CM-7 Least Functionality / SC-7 Boundary Protection / SI-7 Software Integrity
-- Every cluster node must: carry a valid image signature,
-- deny interactive shell access, and reject any-source ingress.
theorem architecture_immutability_invariant (topology : ClusterTopology) :
  (∀ c ∈ topology.nodes,
    (c.immutable_image_signature_valid = true ∧
     c.allows_interactive_shell_access = false ∧
     c.network_ingress_anywhere = false)) → True

-- AU-9 / AU-11 / SI-4 Continuous Monitoring and Audit Record Retention
-- Every log stream must be live, write to a tamper-evident store,
-- and retain records for a minimum of 365 days.
theorem continuous_monitoring_invariant (fabric : LoggingFabric) :
  (∀ l ∈ fabric.streams,
    (l.is_actively_streaming = true ∧
     l.destination_is_tamper_evident = true ∧
     l.retention_days ≥ 365)) → True

The gateway now operates a dual-engine architecture. A Lambda router classifies each incoming telemetry event and dispatches it to the appropriate verification engine. Deterministic, machine-checkable invariants continue to flow through the Lean 4 kernel (Engine 1). Controls that require contextual judgment — reading narrative documents, evaluating training records, assessing vendor risk — are routed to Amazon Bedrock LLM agents powered by Claude (Engine 2). Both engines write structured results to a shared OSCAL Assembler, producing a unified continuous-authorization feed.

Dual-Engine Pipeline

Qualitative Security Clusters (Engine 2)

Five control families verified by Bedrock LLM agents. Each agent grounds its assessment in RAG-retrieved policy documents and emits a structured, schema-validated result that is indistinguishable in the OSCAL output stream from an Engine 1 receipt.

Engine 2 Guardrails

Five layered controls prevent hallucination, enforce output structure, and bound every claim to a verifiable source before results reach the OSCAL Assembler.

Prerequisites

Installation

# 1. Clone the repository
$ git clone https://github.com/j-arndt/fedcloud.git
$ cd fedcloud

# 2. Install Python dependencies
$ python -m venv .venv && source .venv/bin/activate
$ pip install -r requirements.txt

# 3. Install Lean 4 via elan (installs correct toolchain from lean-toolchain)
$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
$ lake build

# 4. Verify the installation
$ python -m pytest tests/ -v
# ✓ 47 passed in 4.21s

Running the Test Suite

The test suite validates both the Python translation layer and the Lean invariant theorems against a suite of synthetic infrastructure fixtures — compliant and non-compliant — to confirm correct PASS / FAIL behavior.

# Run unit tests only (no AWS credentials required)
$ pytest tests/unit/ -v

# Run integration tests (requires valid AWS credentials)
$ pytest tests/integration/ -v --aws-profile fedcloud-ro

# Run Lean theorem tests with synthetic fixtures
$ lake test

# Generate coverage report
$ pytest --cov=src --cov-report=html tests/

Running the Pipeline

# Run a full verification pass against live AWS environment
$ python run_pipeline.py \
    --aws-region us-east-1 \
    --clusters identity crypto architecture monitoring \
    --oscal-out ./oscal-output/ \
    --verbose

# Run a specific cluster only
$ python run_pipeline.py --clusters identity

# Dry-run: translate state and emit Lean source, but do not invoke the kernel
$ python run_pipeline.py --dry-run --snapshot-dir ./snapshots/

# Replay a previously captured snapshot
$ python run_pipeline.py \
    --replay ./snapshots/2026-06-29T00:00:00Z.json \
    --oscal-out ./oscal-output/

Docker Usage

# Pull the published image
$ docker pull ghcr.io/j-arndt/fedcloud:latest

# Run a full pipeline pass (bind-mount credentials and output directory)
$ docker run --rm \
    -e AWS_ACCESS_KEY_ID \
    -e AWS_SECRET_ACCESS_KEY \
    -e AWS_DEFAULT_REGION=us-east-1 \
    -v $(pwd)/oscal-output:/output \
    ghcr.io/j-arndt/fedcloud:latest \
    python run_pipeline.py --oscal-out /output

# Build image locally
$ docker build -t fvg:local .

# Run with AWS instance profile (ECS / EKS task role)
$ docker run --rm \
    --network host \
    -v $(pwd)/oscal-output:/output \
    fvg:local \
    python run_pipeline.py --use-instance-profile --oscal-out /output

Each pipeline run produces three NIST OSCAL 1.1 conformant JSON files. Together they constitute a complete, machine-readable authorization evidence package consumable by GRC tools, agency portals, and the FedRAMP repository.

Verification Receipt — Sample Structure

{
  "verification-receipt": {
    "schema-version": "1.0.0",
    "generated": "2026-06-29T14:32:00Z",
    "pipeline-run-id": "run-a4f2c9b1",
    "kernel": {
      "lean-version": "4.14.0",
      "mathlib-commit": "a9e7c31"
    },
    "results": [
      {
        "theorem-id": "FedCloud.Invariants.identity_least_privilege_invariant",
        "verdict": "PASS",
        "state-hash": "sha256:e3b0c44298fc1c149afb...",
        "timestamp": "2026-06-29T14:30:47Z",
        "control-mappings": [
          "AC-2", "AC-6", "AC-17",
          "IA-2", "IA-2(6)", "IA-5"
        ],
        "counter-example": null
      },
      {
        "theorem-id": "FedCloud.Invariants.cryptographic_protection_invariant",
        "verdict": "FAIL",
        "state-hash": "sha256:e3b0c44298fc1c149afb...",
        "timestamp": "2026-06-29T14:31:02Z",
        "control-mappings": ["SC-8", "SC-28", "SC-28(1)"],
        "counter-example": {
          "resource-type": "S3Bucket",
          "resource-id": "arn:aws:s3:::agency-pii-data-prod",
          "failing-predicate": "is_encrypted_at_rest = false",
          "observed-value": false,
          "required-value": true
        }
      }
    ]
  }
}

SSP Control Implementation Reference

In the updated SSP, each implemented control points to its verification receipt rather than containing a prose implementation statement.

{
  "control-id": "ac-6",
  "description": "Least Privilege",
  "implementation-status": "implemented",
  "proof-evidence": {
    "theorem": "FedCloud.Invariants.identity_least_privilege_invariant",
    "receipt-id": "run-a4f2c9b1/identity_least_privilege_invariant",
    "verdict": "PASS",
    "evaluated-at": "2026-06-29T14:30:47Z"
  }
}

All pipeline configuration can be supplied via command-line flags, environment variables (prefixed FVG_), or a YAML configuration file specified with --config. Command-line flags take precedence over environment variables, which take precedence over the config file.

Exit Codes

Project Directory Structure

The repository root after the hybrid-engine upgrade. The new agents/ directory houses one Bedrock agent definition per qualitative cluster.

fedcloud/
├── agents/                        # Engine 2 — Bedrock agent definitions
│   ├── personnel/                 # KSI-PS: background check + IAM timing
│   │   ├── agent_spec.json        # Bedrock Agent API definition
│   │   ├── action_groups/         # Lambda-backed tool implementations
│   │   └── rag_corpus/            # Approved policy docs for RAG grounding
│   ├── training/                  # KSI-CED: LMS records + recertification
│   ├── incident/                  # KSI-INR: timeline reconstruction + federal reporting
│   ├── recovery/                  # KSI-RPL: DR drill evaluation + RTO/RPO
│   └── supplychain/               # KSI-TPR: SBOM ingestion + CVE analysis
├── lean/                          # Engine 1 — Lean 4 theorem library
│   └── FedCloud/
│       ├── Types.lean             # Inductive data types for infrastructure state
│       └── Invariants.lean        # Security invariant theorems
├── src/                           # Python pipeline orchestrator
│   ├── adapters/                  # Telemetry source adapters
│   ├── lean_bridge/               # JSON → Lean 4 type translator
│   ├── bedrock_runner/            # Bedrock agent invocation + guardrails
│   └── oscal_writer/              # OSCAL artifact assembler
├── lambda/                        # Lambda Router — cluster classification
├── iam/                           # IAM role policies (read-only + per-agent)
├── tests/
│   ├── unit/
│   └── integration/
├── run_pipeline.py                # CLI entry point
└── fvg-config.yml                 # Configuration file (see above)

Configuration File Format

# FedCloud Formal Verification Gateway — configuration file
aws:
  region: us-east-1
  profile: fedcloud-ro

pipeline:
  clusters:
    # Engine 1 — Lean 4 deterministic verification
    - identity
    - crypto
    - architecture
    - monitoring
    # Engine 2 — Bedrock qualitative verification
    - personnel
    - training
    - incident
    - recovery
    - supplychain
  parallel: 2
  timeout: 300

output:
  oscal_dir: ./oscal-output
  snapshot_dir: ./snapshots
  format: oscal
  sign_commits: true
  signing_key_id: ABCDEF1234567890

lean:
  project_dir: ./lean

bedrock:
  model_id: anthropic.claude-3-5-sonnet-20241022-v2:0
  temperature: 0
  knowledge_base_id: KBXXXXXXXX
  agents_dir: ./agents

logging:
  level: INFO