AI & Tensors

ONNX Runtime integration and shape-safe inference.

Shape-safe tensors

Aura supports tensor types that carry shape information.

A tensor with a static shape

AURA

import aura::tensor

val input: Tensor<u32, [2, 2, 3]> = tensor::new<u32>(12)

What gets proven

The checker treats Tensor<T, [d1, d2, ...]> as a value whose shape is part of the type. Verification can then prove that reshape / inference calls never mismatch shapes.

ONNX inference

Load a model and infer:

Inference with a shape-safe output

AURA

import onnxruntime

val model: Model = ai.load_model("identity_u32_2x2x3.onnx")
val out: Tensor<u32, [2, 2, 3]> = model.infer(input)

The verifier checks that the model’s expected input shape matches the provided tensor shape.

Note

This page describes the high-level surface syntax. The plugin-aware verifier emits informational diagnostics like “verified by aura-ai” in the editor (Aura Sentinel).