Vera is designed for LLMs to write. It should also support LLMs as a runtime component, modelled as an algebraic effect:

effect Inference {
  op complete(@String -> @String);
  op embed(@String -> @Array<Float64>);
}

fn classify(@String -> @Category)
  requires(length(@String.0) > 0)
  ensures(true)
  effects(<Inference>)
{
  let @String = complete("Classify as Spam or Ham: " ++ @String.0);
  match parse_category(@String.0) {
    Some(@Category) -> @Category.0,
    None -> Category.Unknown
  }
}

Key design points:

• Effect, not primitive. LLM inference is side-effectful and non-deterministic.
• Testability. A mock handler returns canned responses. No API calls in tests.
• Handler flexibility. One handler uses the Anthropic API, another a local model, another cached replay.
• Contracts still apply. Preconditions on inference inputs are verified normally.
• Constrained decoding potential. Refinement types on return type could eventually guide model output.

The Inference effect belongs in the standard library (Chapter 9).

Spec reference: spec/00-introduction.md § 0.8 "LLM Inference as an Effect"