Design: `@ai_generated` Attribute for Verifiable AI Code

Motivation

When AI (Claude, ChatGPT, etc.) generates code, we need mechanisms to:

Mark code as AI-generated (explicit, auditable)
Require contracts for correctness proof
Verify without external tools or tokens
Certify the verification result

Attribute Definition

// Requires contracts; optional docs string
@ai_generated("prompt used to generate this", language: "claude-3.5-sonnet")
@contract(all(x: int) => result >= x)
fn ai_generated_ceil(x: int) -> int {
  return x;  // Compiler verifies: result >= x
}

// If contracts are missing: COMPILER ERROR
@ai_generated
fn incomplete_ai_code() -> int {
  return 42;  // ✗ error: @ai_generated requires @contract annotations
}

Semantics

1. Attribute Declaration (in lib.rs)

Add to <EXTENSION_KEYWORDS>:

"ai_generated" => Token::AttrAiGenerated,

Add to Node enum:

Node::FunctionDef {
  name: String,
  params: Vec<Param>,
  return_type: Option<Type>,
  body: Box<Node>,
  attributes: Vec<Attribute>,  // ← includes @ai_generated
  // ...
}

enum Attribute {
  Contract(ContractSpec),
  AiGenerated { 
    prompt: Option<String>,
    language: Option<String>,  // "claude-3.5-sonnet", "gpt-4", etc.
  },
  // ...
}

2. Validation Logic (in typechecker.rs)

Rule: If @ai_generated is present on a function:

Function MUST have at least one @contract annotation
Each contract must be satisfiable (Z3 check during compile)
Compiler emits proof certificate (if Z3 succeeds)
If contracts are missing → COMPILER_ERROR, not warning

// In typechecker.rs check_function_attributes()
if let Some(attr) = find_attribute(&attributes, "ai_generated") {
  if !has_contracts(attributes) {
    return Err(diagnostic(
      source_path, span,
      "function with @ai_generated requires @contract annotations"
    ));
  }
  
  // Verify contracts with Z3
  for contract in get_contracts(&attributes) {
    match verify_contract(contract, function_body) {
      Ok(proof) => emit_certificate(proof),
      Err(Unknown) => warn!("contract could not be proven"),
      Err(Unsat) => return Err(diagnostic(..., "contract is false")),
    }
  }
}

3. Contract Formats (Required for @ai_generated)

Functions with @ai_generated must use contracts. Valid formats:

// Pre-condition + post-condition
@contract(all(x: int) => result > 0)  // post-condition
@contract(x > 0 => ...)                // pre-condition
fn sqrt(x: int) -> int { ... }

// Multiple contracts
@contract(x >= 0)  // input precondition
@contract(result >= 0)  // output postcondition
@contract(result * result <= x)  // invariant
fn isqrt(x: int) -> int { ... }

// Loop bounds (for termination)
@contract(loop_bound: 100)
fn iterate(x: int) -> int {
  for i in 0..x { }  // bounded by contract
}

4. Metadata Attributes (Optional)

@ai_generated(
  prompt: "Generate a safe state machine validator for GPIO pins",
  language: "claude-3.5-sonnet",
  timestamp: 2026-06-15T20:00:00Z,
  model_version: "claude-3.5-sonnet-20250615",
  reasoning: "Used extended thinking for 15s"
)
@contract(...)
fn validate_pin_state(pin: u8) -> bool { ... }

Compiler Behavior

Error Examples

❌ Missing contracts
@ai_generated
fn bad_code() -> int {
  return 42;
}
error: function with @ai_generated requires @contract annotations
  → use @contract(result >= 0) or similar

❌ Unproven contract
@ai_generated
@contract(result > 1_000_000)  // too strong for "return 42"
fn weak_proof() -> int {
  return 42;
}
error: contract cannot be proven by Z3
  result > 1_000_000 is false for: result = 42

✓ Valid
@ai_generated
@contract(result >= 0)
fn good_code() -> int {
  return 42;
}
✓ contract verified; proof certificate emitted

Proof Certificate Emission

When a contract is proven:

{
  "function": "good_code",
  "source_file": "example.rz",
  "line": 42,
  "contracts": [
    {
      "assertion": "result >= 0",
      "proven": true,
      "z3_time_ms": 12,
      "proof_hash": "sha256:abc123..."
    }
  ],
  "timestamp": "2026-06-15T20:05:30Z",
  "compiler": "rz v0.2.2"
}

Feature Gate (RES-3501)

Gate @ai_generated behind feature tier:

# LANGUAGE.md

## @ai_generated Attribute
- **Status**: Experimental (v0.2.2+)
- **Stability**: Unstable; may change
- **Requirement**: Functions with @ai_generated MUST have @contract annotations
- **Use case**: Marking code generated by AI tools; enables offline verification

Add to compiler:

if is_experimental_feature("ai_generated") && has_attribute(attributes, "ai_generated") {
  warn!("@ai_generated is experimental and may change");
}

Integration Points

LSP Hover: Show contract status when hovering over @ai_generated function
LSP Diagnostics: Emit actionable errors for missing contracts
MCP Tool (RES-3782): rz_audit_ai_generated(code) → violations
Proof Certificates: Output to JSON for external auditing

Example Workflow

# 1. Claude generates code with contracts
$ cat generated.rz
@ai_generated
@contract(all(x: int) => result == x + 1)
fn increment(x: int) -> int {
  return x + 1;
}

# 2. Compiler checks + verifies
$ rz check generated.rz
✓ contracts verified; proof: sha256:abc123def456

# 3. Emit certificate (optional)
$ rz verify --emit-certs generated.rz > certs.json

# 4. User audits (human + tools)
$ cat certs.json
{
  "proofs": [
    {
      "function": "increment",
      "contract": "all(x: int) => result == x + 1",
      "z3_proven": true,
      ...
    }
  ]
}

# 5. Ship (user removes @ai_generated after review)
# or keep it for continuous verification

Design Decisions

Decision	Rationale
Contracts required	AI code must be explicitly verified; catches mistakes early
Z3-based proof	Local, offline; no token cost; reproducible
Metadata optional	Helps trace code origin; not required for verification
Proof certificates	Auditable; portable; enables external tools to verify
Feature-gated	Allows breaking changes without breaking stable code
No fuzzing gate	@ai_generated is orthogonal to @fuzz; can use both

Limitations & Future Work

Current scope:

Single-function verification (not across files)
Z3 only (not TLA+, bounded model checking, etc.)
No automatic contract inference (user must write contracts)

Future (RES-3780 Phase 2):

Cross-function contract inference (data flow analysis)
Automatic loop bound detection
TLA+ integration for state machine verification
Fuzzer-guided contract weakening

Acceptance Criteria (Implementation)

@ai_generated attribute defined in parser
Validation: requires @contract annotations
Z3 integration: emit proof status
Error messages: guide user to add contracts
Proof certificates: JSON output
LSP support: show contract status in hover
Documentation: LANGUAGE.md + example walkthrough
Tests: 10+ cases (valid, missing contracts, unproven, etc.)

RES-3501: Stability policy (feature tier)
RES-071: Proof certificates
RES-3782: MCP audit tool

Design: @ai_generated Attribute for Verifiable AI Code