Skip to main content

Contracts & Verification

AILANG supports design-by-contract programming through requires and ensures clauses. Contracts make function invariants explicit and machine-checkable.

Research Foundation

This feature implements techniques from the ARC (Automated Reasoning Checks) system developed by AWS:

Bayless et al., "A Neurosymbolic Approach to Natural Language Formalization and Verification" (2025) PDF

ARC demonstrates that formal verification combined with AI code generation dramatically improves correctness. AILANG brings these techniques into the language itself.

Contract Syntax​

Contracts appear after the effect annotation and before the function body:

export func safeDivide(dividend: int, divisor: int) -> int ! {}
requires { divisor != 0 }        -- Precondition: checked at entry
ensures { result >= 0 }          -- Postcondition: checked before return
{
  dividend / divisor
}

Key Elements​

ClausePurposeWhen Checked
requires { ... }Precondition - what must be true when callingFunction entry
ensures { ... }Postcondition - what will be true when returningBefore return
resultSpecial identifier for the return valueOnly in ensures

Multiple Predicates​

Separate multiple predicates with commas:

export func clamp(value: int, min: int, max: int) -> int ! {}
requires { min <= max }
ensures { result >= min, result <= max }
{
  if value < min then min
  else if value > max then max
  else value
}

Basic Example​

This example demonstrates core contract patterns:

examples/runnable/contracts/basic.ail
-- examples/runnable/contracts/basic.ail
-- Basic contract examples demonstrating requires/ensures syntax
-- M-VERIFY: Phase 0 - Contract parsing infrastructure

module examples/runnable/contracts/basic

-- Type definitions for examples
export type Status = OK | FAIL

-- Simple function with precondition
-- requires: x must be non-negative
export func absolute(x: int) -> int ! {}
requires { x >= 0 }
ensures { result >= 0 }
{
  x
}

-- Function with multiple requires predicates
export func safeDivide(dividend: int, divisor: int) -> int ! {}
requires { divisor != 0 }
ensures { result >= 0 }
{
  dividend / divisor
}

-- Function with both requires and ensures
export func increment(x: int, max: int) -> int ! {}
requires { x >= 0 }
ensures { result > x }
{
  if x + 1 > max then max else x + 1
}

-- Function demonstrating 'result' in ensures
export func clamp(value: int, minVal: int, maxVal: int) -> int ! {}
requires { minVal <= maxVal }
ensures { result >= minVal }
{
  if value < minVal then minVal
  else if value > maxVal then maxVal
  else value
}

-- Simple entry point for testing
export func main() -> int ! {}
{
  let a = absolute(5);
  let b = safeDivide(10, 2);
  let c = increment(5, 100);
  let d = clamp(150, 0, 100);
  a + b + c + d
}

Run it:

ailang run --caps IO --entry main examples/runnable/contracts/basic.ail
# Output: 116

Policy Example: Park Admission​

This example reproduces the park admission policy from the ARC paper, demonstrating how AILANG can express the same policy models with machine-checkable contracts.

examples/runnable/contracts/park.ail
-- examples/runnable/contracts/park.ail
-- Reproduces ARC paper park admission example in AILANG
-- From: Bayless et al., "A Neurosymbolic Approach to Natural Language Formalization and Verification" (AWS, 2025)
-- M-VERIFY: Showcase example demonstrating contract-based policy specification

module examples/runnable/contracts/park

-- Type vocabulary (matching ARC's datatypes/variables)
export type Season = LOW_SEASON | HIGH_SEASON
export type AgeClass = CHILD | ADULT | SENIOR
export type AdmissionDecision = ADMIT | DENY

-- Core policy function with contracts
-- ARC rule: "Seniors pay $5 in low season, $10 in high season"
-- ARC rule: "Children under 5 free in low season"
export func admissionFee(age: int, season: Season) -> int ! {}
requires { age >= 0 }
ensures { result >= 0 }
{
  match season {
    LOW_SEASON =>
      if age < 5 then 0
      else if age >= 65 then 5
      else 15,
    HIGH_SEASON =>
      if age >= 65 then 10
      else 20
  }
}

-- Decision function: can visitor enter park given budget?
export func canEnterPark(age: int, season: Season, budget: int) -> AdmissionDecision ! {}
requires { age >= 0 }
{
  let fee = admissionFee(age, season);
  if budget >= fee then ADMIT else DENY
}

-- Age classification helper
export func classifyAge(age: int) -> AgeClass ! {}
requires { age >= 0 }
{
  if age < 5 then CHILD
  else if age >= 65 then SENIOR
  else ADULT
}

-- Entry point for testing
export func main() -> int ! {}
{
  -- Test cases from ARC paper scenarios
  let seniorLow = admissionFee(70, LOW_SEASON);     -- Expected: 5
  let seniorHigh = admissionFee(70, HIGH_SEASON);   -- Expected: 10
  let childLow = admissionFee(3, LOW_SEASON);       -- Expected: 0
  let adultHigh = admissionFee(30, HIGH_SEASON);    -- Expected: 20

  -- Sum of all fees (5 + 10 + 0 + 20 = 35)
  seniorLow + seniorHigh + childLow + adultHigh
}

Run it:

ailang run --caps IO --entry main examples/runnable/contracts/park.ail
# Output: 35 (= 5 + 10 + 0 + 20)

What This Demonstrates​

The park example shows:

  1. Domain modeling with ADTs: Types like Season, AgeClass, and AdmissionDecision capture the policy vocabulary
  2. Business rules as contracts: "Seniors pay $5 in low season" becomes ensures { result >= 0 }
  3. Function composition: canEnterPark builds on admissionFee with contracts propagating
  4. Testable specifications: The main function exercises the policy with known test cases

Why Contracts Matter for AI​

Contracts are particularly valuable for AI code generation:

BenefitExplanation
Specification surfaceAI can read contracts to understand intent
Verification targetGenerated code can be checked against contracts
Confidence scoringMultiple AI-generated implementations can be compared for contract satisfaction
Audit trailContracts document what was specified vs. implemented

The ARC Approach​

The ARC paper demonstrates that:

  1. Having AI generate both contracts and code improves correctness
  2. Redundant generation (multiple samples) + verification catches bugs
  3. Formal specifications make AI reasoning auditable

AILANG implements this pattern natively: contracts are first-class syntax, not comments or annotations.

Runtime Contract Checking​

Enable runtime contract verification with the --verify-contracts flag:

# Compile with contract checks enabled
ailang compile --verify-contracts examples/runnable/contracts/basic.ail -o output/

# Run with contracts (coming in v0.6.2)
ailang run --verify-contracts --caps IO --entry main examples/runnable/contracts/basic.ail

What Gets Generated​

With --verify-contracts: Both documentation comments and panic checks:

func absolute_impl(x interface{}) interface{} {
    // Requires: (x >= 0)
    if !(GeInt(x, int64(0))).(bool) {
        panic("contract violation: requires: (x >= 0) at basic.ail:13:12")
    }
    return x
}

func Absolute(x int64) int64 {
    _result := absolute_impl(x).(int64)
    // Ensures: (result >= 0)
    if !(_result >= int64(0)) {
        panic("contract violation: ensures: (result >= 0) at basic.ail:14:11")
    }
    return _result
}

Without --verify-contracts: Documentation comments only (no runtime overhead):

func absolute_impl(x interface{}) interface{} {
    // Requires: (x >= 0)
    return x
}

Contract Violation Messages​

When a contract is violated at runtime, you get a clear panic message:

panic: contract violation: requires: (divisor != 0) at basic.ail:21:12

The message includes:

  • Contract type (requires or ensures)
  • Original predicate expression
  • Source location (file:line:column)

Current Status​

Implementation Status

Phase 0 + 0.5 Complete (v0.6.2):

  • ✅ Contract syntax (requires/ensures) parses correctly
  • ✅ Contracts stored in Core AST (core.DeclMeta.Contracts)
  • ✅ Runtime checks with --verify-contracts flag
  • ✅ Precondition (requires) checks at function entry
  • ✅ Postcondition (ensures) checks before return
  • ✅ result identifier maps to return value in ensures

Future (Phase 1): SMT-based verification for provably correct code via ailang verify command.

See Also​