Code Review & Safety Audit¶

Audit a payment processing module for OWASP Top 10 vulnerabilities and formally verify authorisation invariants using propositional DPLL and CSF hazard bounding.

GoalInput¶

{
  "goal": "Audit payment processing module for OWASP Top 10 and formally verify authorization invariants",
  "context": "Python FastAPI application handling Stripe payment intents, refunds, and webhook verification. The module gates financial transactions — false positives in authorization checks cause revenue loss, false negatives cause unauthorized charges.",
  "constraints": [
    "All authorization paths must be formally verified (propositional SAT)",
    "CSF hazard probability for code_execute must remain below 0.10",
    "CSF hazard probability for external_api must remain below 0.08",
    "Overall CSF epsilon must not exceed 0.20"
  ],
  "resource_bounds": {
    "max_execution_seconds": 180,
    "max_tokens_per_hour": 100000
  },
  "guardrails": [
    {
      "name": "csf_code_execute",
      "predicate": "csf_hazard",
      "params": {"action": "code_execute", "max_prob": 0.10},
      "message": "Halt if code-execution hazard exceeds 10%"
    }
  ],
  "breakpoints": [
    {
      "name": "pre_report_review",
      "description": "Pause for human review before publishing the security audit report",
      "active": true
    }
  ],
  "subtasks": [
    {
      "goal": "Parse and analyse the payment module's code structure",
      "context": "Use meta_programming to extract all functions, identify authorization checkpoints, and map the call graph from endpoint to Stripe API call.",
      "constraints": ["Extract all functions with their signatures", "Identify decorator-based auth guards"]
    },
    {
      "goal": "Formally verify authorization invariants",
      "context": "Use formal_methods (propositional DPLL) to prove: (user_authenticated AND role_authorized AND session_valid AND csrf_token_valid) -> payment_authorized. Also verify the contrapositive: NOT payment_authorized -> (NOT user_authenticated OR NOT role_authorized OR NOT session_valid OR NOT csrf_token_valid).",
      "constraints": ["Both formula and contrapositive must return SAT", "Strategy: propositional"]
    },
    {
      "goal": "Assess CSF hazard bounds for all pipeline actions",
      "context": "Use align_csf with G6 safety signature. Compute union-bound hazard probability across code_execute (0.10), external_api (0.08), and file_write (0.01) actions. Verify total remains within epsilon=0.20.",
      "constraints": [
        "G6 hazard bounds: code_execute=0.10, external_api=0.08, file_write=0.01",
        "Union bound must not exceed epsilon=0.20"
      ]
    },
    {
      "goal": "Synthesise audit findings into a structured security report",
      "context": "Use agent_claude to produce a report covering: OWASP Top 10 findings, formal verification results, CSF safety scores, and remediation recommendations ranked by severity.",
      "constraints": ["Include severity ratings (Critical/High/Medium/Low)", "Reference formal proof results"]
    }
  ]
}

Pipeline Diagram¶

graph TD
    A[meta_programming<br/>parse + analyse] -->|call graph + functions| B[formal_methods<br/>propositional DPLL]
    A -->|code structure| C[align_csf<br/>hazard bounding]
    B -->|SAT proofs| D[agent_claude<br/>synthesis]
    C -->|safety scores| D
    D --> E((Security Report))

What You Need¶

Tier: Researcher (formal verification) or Builder (with CSF safety framework)
Components: meta_programming, formal_methods, align_csf, agent_claude

Step-by-Step¶

Step 1: Parse the Code¶

{
  "component": "meta_programming",
  "operation": "extract_functions",
  "params": {
    "code": "... payment module source code ..."
  }
}

Then analyse structure:

{
  "component": "meta_programming",
  "operation": "analyze",
  "params": {
    "code": "... payment module source code ..."
  }
}

Returns function signatures, class hierarchy, and dependency information. Use this to identify all authorization checkpoints and the paths from HTTP endpoint to Stripe API call.

Step 2: Verify Authorization Invariants¶

{
  "component": "formal_methods",
  "operation": "verify",
  "params": {
    "formula": "(user_authenticated AND role_authorized AND session_valid AND csrf_token_valid) -> payment_authorized",
    "solver": "propositional"
  }
}

Verify the contrapositive to confirm the invariant is complete:

{
  "component": "formal_methods",
  "operation": "verify",
  "params": {
    "formula": "NOT payment_authorized -> (NOT user_authenticated OR NOT role_authorized OR NOT session_valid OR NOT csrf_token_valid)",
    "solver": "propositional"
  }
}

(formula + solver are the fields of the formal_methods input; solver is one of z3, propositional, prolog, lean. The solver parses the propositional atoms from the formula.)

Why Both Directions?

Proving the forward implication shows that valid credentials grant access. Proving the contrapositive shows that denied access implies at least one credential is invalid — there is no "phantom denial" path.

What a passing check does — and does not — prove

A verified / SAT result means the formal statement holds for the solver, given the formula exactly as written. It does not prove that the formula faithfully captures your real authorization logic. That natural-language → formula translation is the weak link: if the formalisation is wrong, the proof is sound but irrelevant. Read the formula yourself — it is deliberately kept in plain propositional form so a human can check it — and confirm it matches the property you intended before relying on the result.

Step 3: CSF Hazard Assessment¶

align_csf checks one operation at a time against the G6 safety signature — the input is operation + n_steps + epsilon (not a list of actions). Call it once per action in the pipeline:

{
  "component": "align_csf",
  "operation": "check",
  "params": { "operation": "code_execute", "n_steps": 1, "epsilon": 0.20 }
}

Live response (captured from a real call, trimmed to the decision fields):

{
  "operation": "code_execute",
  "per_step_hazard": 0.10,
  "vub": 0.10,
  "epsilon": 0.20,
  "approved": true,
  "explanation": "APPROVED: code_execute × 1 step(s) [correlated] → vub=0.1000 ≤ ε=0.2",
  "completion_state": "qualified-draft",
  "reliability_status": "amber"
}

To bound the combined risk of several actions, check each one and confirm the union bound — the sum of their per-operation vub values — stays within ε:

\[\sum_i \text{vub}_i = 0.10\,(\texttt{code\_execute}) + 0.08\,(\texttt{external\_api}) + 0.01\,(\texttt{file\_write}) = 0.19 \leq \epsilon = 0.20\]

Where these numbers come from

The per-operation hazards in align_csf.G6_SAFETY_SIGNATURE (llm_call=0.05, file_write=0.01, code_execute=0.10, external_api=0.08, rollback=0.001) are assumed priors — engineering defaults, not measured failure rates. The block also records an empirical hazard from observed outcomes per operation; where outcome history exists, that observed rate should be preferred over the prior. Treat the prior as a conservative placeholder, not a calibration.

Step 4: Synthesise the Report¶

{
  "component": "agent_claude",
  "operation": "infer",
  "params": {
    "messages": [
      {
        "role": "user",
        "content": "Produce a structured security audit report for the payment processing module.\n\nFormal verification results: [SAT proofs inserted]\nCSF hazard assessment: [scores inserted]\nCode analysis: [meta_programming output inserted]\n\nFormat: OWASP Top 10 findings with severity ratings, formal proof references, and remediation recommendations."
      }
    ],
    "max_tokens": 4096
  }
}

What Happened¶

G6 orchestrated three intelligence classes:

Self-Modification (meta_programming) parsed code structure and extracted authorization checkpoints
Formal Methods checked authorization invariants via propositional DPLL — a SAT result means the property holds for the solver, given the formula, not a real-world guarantee
Alignment (align_csf) computed union-bound hazard probabilities and verified they stay within epsilon
Synthesis (agent_claude) produced a structured report combining all three evidence streams

Why G6 Over a Bare LLM¶

A capable LLM can spot bugs and suggest improvements in a code review. G6 adds deterministic formal verification (SAT proofs for authorization properties) and CSF hazard bounds that are auditable and reproducible — not probabilistic opinions. Prebuilt templates wire static analysis, formal methods, and safety checks into a single pipeline triggered by one GoalInput JSON.