A minimal, mathematically verifiable ONNX runtime implementation in Rust.
Fast, fearless, and formally verified ONNX in Rust.
This project provides a minimal, educational ONNX runtime implementation focused on:
- Simplicity: Easy to understand and modify
- Verifiability: Formal mathematical verification using Why3 and property-based testing
- Performance: Efficient operations using ndarray
- Safety: Memory-safe Rust implementation with mathematical guarantees
- β Dual Format Support: JSON and binary ONNX protobuf formats with automatic detection
- β
Graph Visualization: Beautiful terminal ASCII art and professional Graphviz export
- Terminal visualization with dynamic layout and rich formatting
- DOT format export for publication-quality diagrams (PNG, SVG, PDF)
- CLI integration with
--graph
and--dot
options - Topological sorting and cycle detection
- β
Comprehensive Operator Support: Wide range of ONNX operators for various model types
- Core Operations:
Add
,Mul
,MatMul
,Conv
,Relu
,Sigmoid
,Reshape
,Transpose
- Advanced Operations:
Concat
,Slice
,Upsample
,MaxPool
,Softmax
,NonMaxSuppression
- Computer Vision: Support for CNN architectures and object detection models
- Tested Compatibility: Validated with real-world models including YOLOv8
- Core Operations:
- β Formal Verification: Mathematical specifications with Why3 and property-based testing
- β
Production Ready Features:
- Model loading and validation with comprehensive error handling
- Async support for high-throughput inference
- Benchmarking and performance monitoring
- Command-line tools for model testing and visualization
- Comprehensive examples and documentation
RunNX requires the Protocol Buffers compiler (protoc
) to build:
# Ubuntu/Debian
sudo apt-get install protobuf-compiler
# macOS
brew install protobuf
# Windows
choco install protoc
Add this to your Cargo.toml
:
[dependencies]
runnx = "0.2.0"
use runnx::{Model, Tensor};
// Load a model (supports both JSON and ONNX binary formats)
let model = Model::from_file("model.onnx")?; // Auto-detects format
// Or explicitly:
// let model = Model::from_onnx_file("model.onnx")?; // Binary ONNX
// let model = Model::from_json_file("model.json")?; // JSON format
// Create input tensor
let input = Tensor::from_array(ndarray::array![[1.0, 2.0, 3.0]]);
// Run inference
let outputs = model.run(&[("input", input)])?;
// Get results
let result = outputs.get("output").unwrap();
println!("Result: {:?}", result.data());
RunNX supports various computer vision models. Here's an example with object detection:
use runnx::Model;
// Load any compatible ONNX model (e.g., classification, detection, segmentation)
let model = Model::from_file("vision_model.onnx")?;
// For object detection models like YOLOv8, RCNN, etc.
// The runtime handles various operator types automatically
cargo run --example yolov8_detect_and_draw // YOLOv8 detection example
use runnx::Model;
let model = /* ... create or load model ... */;
// Save in different formats
model.to_file("output.onnx")?; // Auto-detects format from extension
model.to_onnx_file("binary.onnx")?; // Explicit binary ONNX format
model.to_json_file("readable.json")?; // Explicit JSON format
# Run inference on a model (supports both .onnx and .json files)
cargo run --bin runnx-runner -- --model model.onnx --input input.json
cargo run --bin runnx-runner -- --model model.json --input input.json
# Show model summary and graph visualization
cargo run --bin runnx-runner -- --model model.onnx --summary --graph
# Generate Graphviz DOT file for professional diagrams
cargo run --bin runnx-runner -- --model model.onnx --dot graph.dot
# Run specialized examples (computer vision, object detection, etc.)
cargo run --example yolov8_detect_and_draw # Object detection example
# Run async inference (requires --features async)
cargo run --features async --bin runnx-runner -- --model model.onnx --input input.json
RunNX provides comprehensive graph visualization capabilities to help you understand and debug ONNX model structures. You can visualize models both in the terminal and as publication-quality graphics.
Display beautiful ASCII art representations of your model directly in the terminal:
# Show visual graph representation
./target/debug/runnx-runner --model model.onnx --graph
# Show both model summary and graph
./target/debug/runnx-runner --model model.onnx --summary --graph
Here's what the terminal visualization looks like for a complex neural network:
ββββββββββββββββββββββββββββββββββββββββββ
β GRAPH: neural_network_demo β
ββββββββββββββββββββββββββββββββββββββββββ
π₯ INPUTS:
ββ image_input [1 Γ 3 Γ 224 Γ 224] (float32)
ββ mask_input [1 Γ 1 Γ 224 Γ 224] (float32)
βοΈ INITIALIZERS:
ββ conv1_weight [64 Γ 3 Γ 7 Γ 7]
ββ conv1_bias [64]
ββ fc_weight [1000 Γ 512]
ββ fc_bias [1000]
π COMPUTATION FLOW:
β
ββ Step 1: conv1
β ββ Operation: Conv
β ββ Inputs:
β β ββ image_input
β β ββ conv1_weight
β β ββ conv1_bias
β ββ Outputs:
β β ββ conv1_output
β ββ Attributes:
β ββ kernel_shape: [7, 7]
β ββ strides: [2, 2]
β ββ pads: [3, 3, 3, 3]
β
ββ Step 2: relu1
β ββ Operation: Relu
β ββ Inputs:
β β ββ conv1_output
β ββ Outputs:
β β ββ relu1_output
β ββ (no attributes)
[... more steps ...]
π€ OUTPUTS:
ββ classification [1 Γ 1000] (float32)
ββ segmentation [1 Γ 21 Γ 224 Γ 224] (float32)
π STATISTICS:
ββ Total nodes: 10
ββ Input tensors: 2
ββ Output tensors: 2
ββ Initializers: 4
π― OPERATION SUMMARY:
ββ Add: 1
ββ Conv: 2
ββ Flatten: 1
ββ GlobalAveragePool: 1
ββ MatMul: 1
ββ MaxPool: 1
ββ Mul: 1
ββ Relu: 1
ββ Upsample: 1
Generate professional diagrams using DOT format for Graphviz:
# Generate DOT file for Graphviz
./target/debug/runnx-runner --model model.onnx --dot graph.dot
# Convert to PNG (requires Graphviz installation)
dot -Tpng graph.dot -o graph.png
# Convert to SVG for vector graphics
dot -Tsvg graph.dot -o graph.svg
# Convert to PDF for documents
dot -Tpdf graph.dot -o graph.pdf
The DOT format generates clean, professional diagrams with:
- Green ellipses for input tensors
- Blue diamonds for initializers (weights/biases)
- Rectangular boxes for operations
- Red ellipses for output tensors
- Directed arrows showing data flow
Example: Multi-task neural network with classification and segmentation branches
The generated DOT file contains structured graph data that Graphviz uses to create the visualizations. Here's an excerpt of the DOT format:
digraph G {
rankdir=TB;
node [shape=box, style=rounded];
"image_input" [shape=ellipse, color=green, label="image_input"];
"mask_input" [shape=ellipse, color=green, label="mask_input"];
"conv1_weight" [shape=diamond, color=blue, label="conv1_weight"];
"conv1_bias" [shape=diamond, color=blue, label="conv1_bias"];
"conv1" [label="conv1\n(Conv)"];
"relu1" [label="relu1\n(Relu)"];
"classification" [shape=ellipse, color=red, label="classification"];
"segmentation" [shape=ellipse, color=red, label="segmentation"];
"image_input" -> "conv1";
"conv1_weight" -> "conv1";
"conv1_bias" -> "conv1";
"conv1" -> "relu1";
"relu1" -> "classification";
// ... additional connections
}
The DOT format uses:
- Nodes: Define graph elements with shapes, colors, and labels
- Edges: Define connections with
->
arrows - Attributes: Control visual appearance and layout
- rankdir=TB: Top-to-bottom layout direction
For the complete DOT file example, see assets/complex_graph.dot
.
You can also generate visualizations programmatically:
use runnx::Model;
let model = Model::from_file("model.onnx")?;
// Print graph to terminal
model.print_graph();
// Generate DOT format
let dot_content = model.to_dot();
std::fs::write("graph.dot", dot_content)?;
// The graph name box automatically adjusts to any length
// Works with short names like "CNN" or very long names like
// "SuperLongComplexNeuralNetworkGraphName"
- Dynamic Layout: Graph title box automatically adjusts to accommodate any name length
- Topological Sorting: Shows correct execution order with dependency resolution
- Cycle Detection: Gracefully handles graphs with cycles
- Rich Information: Displays shapes, data types, attributes, and statistics
- Color Coding: Visual distinction between different node types in DOT format
- Multiple Formats: Terminal ASCII art and Graphviz-compatible DOT export
- Professional Quality: Publication-ready graphics for papers and presentations
The runtime is organized into several key components:
- Model: ONNX model representation and loading
- Graph: Computational graph with nodes and edges
- Tensor: N-dimensional array wrapper with type safety
- Operators: Implementation of ONNX operations
- Runtime: Execution engine with optimizations
RunNX supports both JSON and binary ONNX protobuf formats:
- Human-readable: Easy to inspect and debug
- Text-based: Can be viewed and edited in any text editor
- Larger file size: More verbose due to text representation
- Extension:
.json
- Standard format: Official ONNX protobuf serialization
- Compact: Smaller file sizes due to binary encoding
- Interoperable: Compatible with other ONNX runtime implementations
- Extension:
.onnx
The Model::from_file()
method automatically detects the format based on file extension:
.onnx
files β Binary ONNX protobuf format.json
files β JSON format- Other extensions β Attempts JSON parsing as fallback
For explicit control, use:
Model::from_onnx_file()
for binary ONNX filesModel::from_json_file()
for JSON files
Operator | Status | Notes |
---|---|---|
Add |
β | Element-wise addition |
Mul |
β | Element-wise multiplication |
MatMul |
β | Matrix multiplication |
Conv |
β | 2D Convolution |
Relu |
β | Rectified Linear Unit |
Sigmoid |
β | Sigmoid activation |
Reshape |
β | Tensor reshaping |
Transpose |
β | Tensor transposition |
Operator | Status | Notes |
---|---|---|
Concat |
β | Tensor concatenation |
Slice |
β | Tensor slicing operations |
Upsample |
β | Feature map upsampling |
MaxPool |
β | Max pooling operations |
Softmax |
β | Softmax normalization |
NonMaxSuppression |
β | Non-maximum suppression |
Legend: β = Fully implemented, π§ = In development, β = Not implemented
Model Compatibility: These operators enable support for various model architectures including:
- Computer Vision: CNNs, ResNet, EfficientNet, Vision Transformers
- Object Detection: YOLO family (YOLOv8, YOLOv5), R-CNN variants, SSD
- Classification: Image classifiers and feature extractors
- Custom Models: Any ONNX model using the supported operator set
use runnx::{Model, Tensor};
use std::collections::HashMap;
fn main() -> Result<(), Box<dyn std::error::Error>> {
// Load model from file
let model = Model::from_file("path/to/model.onnx")?;
// Print model information
println!("Model: {}", model.name());
println!("Inputs: {:?}", model.input_names());
println!("Outputs: {:?}", model.output_names());
// Prepare inputs
let mut inputs = HashMap::new();
inputs.insert("input", Tensor::zeros(&[1, 3, 224, 224]));
// Run inference
let outputs = model.run(&inputs)?;
// Process outputs
for (name, tensor) in outputs {
println!("Output '{}': shape {:?}", name, tensor.shape());
}
Ok(())
}
RunNX supports various computer vision models including object detection:
# Object detection example (YOLOv8)
cargo run --example yolov8_detect_and_draw
# Expected workflow:
# 1. Model loading and validation
# 2. Image preprocessing (resize, normalize)
# 3. Inference execution
# 4. Post-processing (NMS, confidence filtering)
# 5. Visualization (bounding boxes, labels)
use runnx::*;
fn main() -> runnx::Result<()> {
// Create a simple model
let mut graph = graph::Graph::new("demo_graph".to_string());
// Add input/output specifications
let input_spec = graph::TensorSpec::new("input".to_string(), vec![Some(1), Some(4)]);
let output_spec = graph::TensorSpec::new("output".to_string(), vec![Some(1), Some(4)]);
graph.add_input(input_spec);
graph.add_output(output_spec);
// Add a ReLU node
let relu_node = graph::Node::new(
"relu_1".to_string(),
"Relu".to_string(),
vec!["input".to_string()],
vec!["output".to_string()],
);
graph.add_node(relu_node);
let model = model::Model::with_metadata(
model::ModelMetadata {
name: "demo_model".to_string(),
version: "1.0".to_string(),
description: "A simple ReLU demo model".to_string(),
producer: "RunNX Demo".to_string(),
onnx_version: "1.9.0".to_string(),
domain: "".to_string(),
},
graph,
);
// Save in both formats
model.to_json_file("demo_model.json")?;
model.to_onnx_file("demo_model.onnx")?;
// Load from both formats
let json_model = model::Model::from_json_file("demo_model.json")?;
let onnx_model = model::Model::from_onnx_file("demo_model.onnx")?;
// Auto-detection also works
let auto_json = model::Model::from_file("demo_model.json")?;
let auto_onnx = model::Model::from_file("demo_model.onnx")?;
println!("β
All formats loaded successfully!");
println!("Original: {}", model.name());
println!("JSON: {}", json_model.name());
println!("ONNX: {}", onnx_model.name());
Ok(())
}
use runnx::{Model, Tensor};
use ndarray::Array2;
fn main() -> Result<(), Box<dyn std::error::Error>> {
// Initialize logging
env_logger::init();
// Create a simple linear transformation: y = x * w + b
let weights = Array2::from_shape_vec((3, 2), vec![0.5, 0.3, 0.2, 0.4, 0.1, 0.6])?;
let bias = Array2::from_shape_vec((1, 2), vec![0.1, 0.2])?;
let input = Tensor::from_array(Array2::from_shape_vec((1, 3), vec![1.0, 2.0, 3.0])?);
let w_tensor = Tensor::from_array(weights);
let b_tensor = Tensor::from_array(bias);
// Manual computation for verification
let result1 = input.matmul(&w_tensor)?;
let result2 = result1.add(&b_tensor)?;
println!("Linear transformation result: {:?}", result2.data());
Ok(())
}
# Basic model operations and format compatibility
cargo run --example onnx_demo
cargo run --example simple_model
cargo run --example format_conversion
# Computer vision applications
cargo run --example yolov8_detect_and_draw # Object detection example
cargo run --example yolov8_object_detection # Detection with post-processing
cargo run --example yolov8n_compat_demo # Model compatibility testing
# Core functionality
cargo run --example tensor_ops # Tensor operations
cargo run --example formal_verification # Mathematical verification
cargo run --example test_onnx_support # Operator support testing
use runnx::*;
fn create_simple_model() -> runnx::Result<()> {
// Create a simple neural network model
let mut graph = graph::Graph::new("custom_model".to_string());
// Define inputs and outputs
let input_spec = graph::TensorSpec::new("input".to_string(), vec![Some(1), Some(4)]);
let output_spec = graph::TensorSpec::new("output".to_string(), vec![Some(1), Some(4)]);
graph.add_input(input_spec);
graph.add_output(output_spec);
// Add operations
let relu_node = graph::Node::new(
"activation".to_string(),
"Relu".to_string(),
vec!["input".to_string()],
vec!["output".to_string()],
);
graph.add_node(relu_node);
// Create model with metadata
let model = model::Model::with_metadata(
model::ModelMetadata {
name: "custom_neural_network".to_string(),
version: "1.0".to_string(),
description: "Custom model example".to_string(),
producer: "RunNX".to_string(),
onnx_version: "1.9.0".to_string(),
domain: "".to_string(),
},
graph,
);
// Save in multiple formats
model.to_json_file("custom_model.json")?;
model.to_onnx_file("custom_model.onnx")?;
println!("β
Custom model created and saved!");
Ok(())
}
graph.add_node(silu_sigmoid);
graph.add_node(silu_mul);
// Multi-scale feature processing
let upsample = graph::Node::new(
"upsample".to_string(),
"Upsample".to_string(),
vec!["silu_out".to_string()],
vec!["upsampled".to_string()],
);
let concat = graph::Node::new(
"concat".to_string(),
"Concat".to_string(),
vec!["upsampled".to_string(), "silu_out".to_string()],
vec!["concat_out".to_string()],
);
graph.add_node(upsample);
graph.add_node(concat);
// Detection head with Softmax
let head_conv = graph::Node::new(
"head_conv".to_string(),
"Conv".to_string(),
vec!["concat_out".to_string()],
vec!["raw_detections".to_string()],
);
let softmax = graph::Node::new(
"softmax".to_string(),
"Softmax".to_string(),
vec!["raw_detections".to_string()],
vec!["detections".to_string()],
);
graph.add_node(head_conv);
graph.add_node(softmax);
let model = model::Model::with_metadata(
model::ModelMetadata {
name: "yolo_demo_v1".to_string(),
version: "1.0".to_string(),
description: "YOLO-like object detection model".to_string(),
producer: "RunNX YOLO Demo".to_string(),
onnx_version: "1.9.0".to_string(),
domain: "".to_string(),
},
graph,
);
println!("π― YOLO Model Created!");
println!(" Inputs: {} ({})", model.graph.inputs.len(), model.graph.inputs[0].name);
println!(" Outputs: {} ({})", model.graph.outputs.len(), model.graph.outputs[0].name);
println!(" Nodes: {} (Conv, SiLU, Upsample, Concat, Softmax)", model.graph.nodes.len());
Ok(())
}
### Basic Model Loading
```rust
use runnx::{Model, Tensor};
use std::collections::HashMap;
fn main() -> Result<(), Box<dyn std::error::Error>> {
// Load model from file
let model = Model::from_file("path/to/model.onnx")?;
// Print model information
println!("Model: {}", model.name());
println!("Inputs: {:?}", model.input_names());
println!("Outputs: {:?}", model.output_names());
// Prepare inputs
let mut inputs = HashMap::new();
inputs.insert("input", Tensor::zeros(&[1, 3, 224, 224]));
// Run inference
let outputs = model.run(&inputs)?;
// Process outputs
for (name, tensor) in outputs {
println!("Output '{}': shape {:?}", name, tensor.shape());
}
Ok(())
}
The runtime includes benchmarking capabilities:
# Run benchmarks
cargo bench
# Generate HTML reports
cargo bench -- --output-format html
Example benchmark results:
- Basic operations: ~10-50 Β΅s
- Small model inference: ~100-500 Β΅s
- Medium model inference: ~1-10 ms
RunNX includes comprehensive formal verification capabilities to ensure mathematical correctness:
The runtime includes formal specifications for all tensor operations using Why3:
(** Addition operation specification *)
function add_spec (a b: tensor) : tensor
requires { valid_tensor a /\ valid_tensor b }
requires { a.shape = b.shape }
ensures { valid_tensor result }
ensures { result.shape = a.shape }
ensures { forall i. 0 <= i < length result.data ->
result.data[i] = a.data[i] + b.data[i] }
Automatic verification of mathematical properties:
use runnx::formal::contracts::{AdditionContracts, ActivationContracts, YoloOperatorContracts};
// Test addition commutativity: a + b = b + a
let result1 = tensor_a.add_with_contracts(&tensor_b)?;
let result2 = tensor_b.add_with_contracts(&tensor_a)?;
assert_eq!(result1.data(), result2.data());
// Test ReLU idempotency: ReLU(ReLU(x)) = ReLU(x)
let relu_once = tensor.relu_with_contracts()?;
let relu_twice = relu_once.relu_with_contracts()?;
assert_eq!(relu_once.data(), relu_twice.data());
// Test Softmax probability distribution: sum = 1.0
let softmax_result = tensor.softmax_with_contracts()?;
let sum: f32 = softmax_result.data().iter().sum();
assert!((sum - 1.0).abs() < 1e-6);
Dynamic checking of invariants during execution:
use runnx::formal::runtime_verification::InvariantMonitor;
let monitor = InvariantMonitor::new();
let result = tensor.add(&other)?;
// Verify numerical stability and bounds
assert!(monitor.verify_operation(&[&tensor, &other], &[&result]));
The formal verification system proves:
- Addition: Commutativity, associativity, identity
- Matrix Multiplication: Associativity, distributivity
- ReLU: Idempotency, monotonicity, non-negativity
- Sigmoid: Boundedness (0, 1), monotonicity, symmetry
- Numerical Stability: Overflow/underflow prevention
# Install Why3 (optional, for complete formal proofs)
make -C formal install-why3
# Run all verification (tests + proofs)
make -C formal all
# Run only property-based tests (no Why3 required)
cargo test formal --lib
# Run verification example
cargo run --example formal_verification
# Generate verification report
make -C formal report
RunNX includes a Justfile with convenient shortcuts for common development tasks:
# Install just command runner (one time setup)
cargo install just
# Show all available commands
just --list
# Quick development cycle
just dev # Format, lint, and test
just test # Run all tests
just build # Build the project
just examples # Run all examples
# Code quality
just format # Format code
just lint # Run clippy
just quality # Run quality check script
# Documentation
just docs-open # Build and open docs
# Benchmarks
just bench # Run benchmarks
# Formal verification
just formal-test # Test formal verification setup
# CI simulation
just ci # Simulate CI checks locally
Alternatively, if you don't have just
installed, use the included shell script:
# Show all available commands
./dev.sh help
# Quick development cycle
./dev.sh dev # Format, lint, and test
./dev.sh test # Run all tests
./dev.sh examples # Run all examples
# Run all tests
cargo test
# or with just
just test
# Run tests with logging
RUST_LOG=debug cargo test
# Run specific test
cargo test test_tensor_operations
# Build and open documentation
cargo doc --open
# or with just
just docs-open
# Build with private items
cargo doc --document-private-items
We welcome contributions! Please follow our development quality standards:
- Fork the repository
- Create a feature branch
- Make your changes following our Development QA Guidelines
- Add tests and documentation
- Run quality checks:
./scripts/quality-check.sh
- Commit your changes (pre-commit hooks will run automatically)
- Submit a pull request
RunNX uses automated quality assurance tools to maintain code quality:
- Pre-commit hooks: Automatically run formatting, linting, and tests before each commit
- Code formatting: Consistent style enforced by
rustfmt
- Linting: Comprehensive checks with
clippy
(warnings treated as errors) - Comprehensive testing: Unit tests, integration tests, property-based tests, and doc tests
- Build verification: Ensures all code compiles successfully
For detailed information, see Development QA Guidelines.
To run quality checks manually:
# Run all quality checks with auto-fixes
./scripts/quality-check.sh
# Or run individual checks
cargo fmt # Format code
cargo clippy # Run linting
cargo test # Run all tests
This project is licensed under
- Apache License, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
- ONNX - Open Neural Network Exchange format
- ndarray - Rust's
ndarray
library - Candle - Inspiration for some design patterns
- Dual Format Support: Both JSON and binary ONNX protobuf formats
- Auto-detection: Automatic format detection based on file extension
- Graph Visualization: Terminal ASCII art and professional Graphviz export
- Core Operators: Add, Mul, MatMul, Conv, ReLU, Sigmoid, Reshape, Transpose
- YOLO Operators: Concat, Slice, Upsample, MaxPool, Softmax, NonMaxSuppression
- Formal Verification: Mathematical specifications with Why3
- CLI Tool: Command-line runner with visualization capabilities
- Performance Optimizations: GPU acceleration and SIMD vectorization
- Extended ONNX Support: Additional operators (BatchNorm, LayerNorm, etc.)
- Quantization: INT8 and FP16 model support
- Model Optimization: Graph optimization passes and operator fusion
- Deployment Targets: WASM compilation and embedded systems support
- Language Bindings: Python and JavaScript bindings
- Enterprise Features: Model serving and distributed inference
- Advanced Visualization: Interactive model exploration tools
- Release Notes - What's new in the latest version
- Complete Changelog - Full history of changes
- Release History - All previous release notes
- Contributing Guide - How to contribute to RunNX
- Development QA - Quality assurance guidelines
- Formal Verification - Mathematical verification details
- API Documentation - Complete API reference
- Crates.io - Package information
- GitHub Repository - Source code and issues
- CI/CD Status - Build and test results