Examples

These examples are organized from simple symbolic construction to full-model interpretation.

• Example: Manual Bounds on an Affine + ReLU Graph
• Example: Verify an MLP with zono.interpret
• Example: Transformer-Style Attention Block
• Example: Export a BoundLab VNN Pipeline to ONNX
• Example: Differential Verification with diff.zono3

Choosing an Example

• Start with Example: Manual Bounds on an Affine + ReLU Graph to learn expression and bound APIs.

• Continue with Example: Verify an MLP with zono.interpret to verify an exported MLP graph.

• Example: Transformer-Style Attention Block covers transformer-style operations (matmul, softmax).

• Example: Export a BoundLab VNN Pipeline to ONNX shows how to export a BoundLab verification pipeline to ONNX.

• Example: Differential Verification with diff.zono3 demonstrates certifying bounds on the difference between two networks.