GlassBoxAI-RNN is a comprehensive, production-ready Recurrent Neural Network implementation suite featuring:
- Multiple GPU backends: CUDA and OpenCL acceleration
- Multiple language implementations: C++ and Rust
- Facade pattern architecture: Clean API separation with deep introspection capabilities
- Formal verification: Kani-verified Rust implementation for memory safety guarantees
- Multiple cell types: SimpleRNN, LSTM, and GRU architectures
- CISA/NSA Secure by Design compliance: Built following government cybersecurity standards
This project demonstrates enterprise-grade software engineering practices including comprehensive testing, formal verification, cross-platform compatibility, and security-first development.
- Features
- Architecture
- File Structure
- Prerequisites
- Installation & Compilation
- CLI Reference
- Testing
- Formal Verification with Kani
- CISA/NSA Compliance
- License
- Author
| Feature | Description |
|---|---|
| Cell Types | SimpleRNN, LSTM, and GRU architectures |
| Multi-Layer Support | Configurable stacked hidden layers |
| Training | Backpropagation Through Time (BPTT) with gradient clipping |
| Activation Functions | Sigmoid, Tanh, ReLU, Linear |
| Loss Functions | MSE, Cross-Entropy with stable softmax |
| Model Persistence | JSON serialization for model save/load |
| Dropout | Regularization support during training |
| Sequence Learning | Variable-length sequence processing |
| Backend | Implementation | Performance |
|---|---|---|
| CUDA | Native CUDA kernels | Optimal for NVIDIA GPUs |
| OpenCL | Cross-platform GPU | AMD, Intel, NVIDIA support |
| Feature | Technology |
|---|---|
| Memory Safety | Rust ownership model |
| Formal Verification | Kani proof harnesses |
| Bounds Checking | Verified array access |
| Input Validation | CLI argument validation |
┌─────────────────────────────────────────────────────────────────────┐
│ GlassBoxAI-RNN │
├─────────────────────────────────────────────────────────────────────┤
│ │
│ ┌─────────────┐ ┌─────────────┐ ┌─────────────────────────────┐ │
│ │ C++ CUDA │ │ C++ OpenCL │ │ Rust CUDA │ │
│ ├─────────────┤ ├─────────────┤ ├─────────────────────────────┤ │
│ │ • rnn.cu │ │ • rnn_ │ │ • rust_cuda/ │ │
│ │ • facaded_ │ │ opencl.cpp│ │ • facaded_rust_cuda/ │ │
│ │ rnn.cu │ │ • facaded_ │ │ └─ kani/ │ │
│ │ │ │ rnn_ │ │ (Formal Verification) │ │
│ │ │ │ opencl.cpp│ │ │ │
│ └─────────────┘ └─────────────┘ └─────────────────────────────┘ │
│ │
│ ┌─────────────────────────────────────────────────────────────────┐│
│ │ Shared Features ││
│ │ • Consistent CLI interface across all implementations ││
│ │ • JSON compatible model formats ││
│ │ • Comprehensive test suites ││
│ └─────────────────────────────────────────────────────────────────┘│
│ │
└─────────────────────────────────────────────────────────────────────┘
GlassBoxAI-RNN/
│
├── rnn.cpp # C++ CPU RNN implementation
├── rnn.cu # C++ CUDA RNN implementation
├── rnn_opencl.cpp # C++ OpenCL RNN implementation
├── facaded_rnn.cpp # C++ CPU RNN with Facade pattern
├── facaded_rnn.cu # C++ CUDA RNN with Facade pattern
├── facaded_rnn_opencl.cpp # C++ OpenCL RNN with Facade pattern
│
├── rust_cuda/ # Rust CUDA RNN implementation
│ ├── Cargo.toml
│ └── src/
│ └── main.rs
│
├── facaded_rust_cuda/ # Rust CUDA RNN with Facade pattern
│ ├── Cargo.toml
│ └── src/
│ ├── main.rs
│ └── kani/ # Kani proof harnesses
│
├── rnn_cuda_tests.sh # CUDA test suite
├── rnn_opencl_tests.sh # OpenCL test suite
├── rnn_cpp_tests.sh # C++ test suite
│
├── license.md # MIT License
└── README.md # This file
| Dependency | Version | Purpose |
|---|---|---|
| GCC/G++ | 11+ | C++ compilation |
| CUDA Toolkit | 12.0+ | CUDA compilation |
| Rust | 1.75+ | Rust compilation |
| Dependency | Version | Purpose |
|---|---|---|
| OpenCL SDK | 3.0 | OpenCL compilation |
| Kani | 0.67+ | Formal verification |
# Standard RNN
nvcc -O2 -o rnn_cuda rnn.cu
# Facade RNN
nvcc -O2 -o facaded_rnn_cuda facaded_rnn.cu# Standard RNN
g++ -O2 -std=c++11 -o rnn_opencl rnn_opencl.cpp -lOpenCL
# Facade RNN
g++ -O2 -std=c++11 -o facaded_rnn_opencl facaded_rnn_opencl.cpp -lOpenCL# Standard RNN
g++ -O2 -std=c++11 -o rnn rnn.cpp
# Facade RNN
g++ -O2 -std=c++11 -o facaded_rnn facaded_rnn.cpp# Standard RNN
cd rust_cuda
cargo build --release
# Facade RNN
cd facaded_rust_cuda
cargo build --release# Build everything
nvcc -O2 -o rnn_cuda rnn.cu
nvcc -O2 -o facaded_rnn_cuda facaded_rnn.cu
g++ -O2 -std=c++11 -o rnn_opencl rnn_opencl.cpp -lOpenCL
g++ -O2 -std=c++11 -o facaded_rnn_opencl facaded_rnn_opencl.cpp -lOpenCL
g++ -O2 -std=c++11 -o rnn rnn.cpp
g++ -O2 -std=c++11 -o facaded_rnn facaded_rnn.cpp
(cd rust_cuda && cargo build --release)
(cd facaded_rust_cuda && cargo build --release)The standard RNN implementations provide core recurrent neural network functionality.
rnn_cuda <command> [options]
rnn_opencl <command> [options]
rust_cuda/target/release/rnn_cuda <command> [options]
| Command | Description |
|---|---|
create |
Create a new RNN model |
train |
Train the model with data |
predict |
Make predictions with a trained model |
info |
Display model information |
help |
Show help message |
| Option | Description |
|---|---|
--input=N |
Input layer size (required) |
--hidden=N,N,... |
Hidden layer sizes (required) |
--output=N |
Output layer size (required) |
--save=FILE.json |
Save model to JSON file (required) |
--cell=TYPE |
simplernn|lstm|gru (default: lstm) |
--lr=VALUE |
Learning rate (default: 0.01) |
--hidden-act=TYPE |
sigmoid|tanh|relu|linear (default: tanh) |
--output-act=TYPE |
sigmoid|tanh|relu|linear (default: linear) |
--loss=TYPE |
mse|crossentropy (default: mse) |
--clip=VALUE |
Gradient clipping (default: 5.0) |
--bptt=N |
BPTT steps (default: 0 = full sequence) |
| Option | Description |
|---|---|
--model=FILE.json |
Load model from JSON file (required) |
--data=FILE.csv |
Training data CSV file (required) |
--save=FILE.json |
Save trained model to JSON (required) |
--epochs=N |
Number of training epochs (default: 100) |
--batch=N |
Batch size (default: 1) |
--lr=VALUE |
Override learning rate |
--seq-len=N |
Sequence length (default: auto-detect) |
--verbose |
Verbose output |
| Option | Description |
|---|---|
--model=FILE.json |
Load model from JSON file (required) |
--input=v1,v2,... |
Input values as CSV (required) |
| Option | Description |
|---|---|
--model=FILE.json |
Load model from JSON file (required) |
# Create an LSTM model
rnn_cuda create --input=2 --hidden=16,16 --output=2 --cell=lstm --save=model.json
# Train the model
rnn_cuda train --model=model.json --data=train.csv --epochs=100 --save=model_trained.json
# Make predictions
rnn_cuda predict --model=model_trained.json --input=0.5,0.5
# Display model info
rnn_cuda info --model=model.jsonThe Facade implementations include all standard commands plus deep introspection capabilities for research and debugging.
| Command | Description |
|---|---|
query |
Query model state and internals |
| Option | Description |
|---|---|
--model=FILE.json |
Load model from JSON file (required) |
--query-type=TYPE |
Query type (required) |
--layer=N |
Layer index |
--timestep=N |
Timestep index |
--neuron=N |
Neuron index |
--index=N |
Generic index parameter |
--dropout-rate=VALUE |
Set dropout rate (0.0-1.0) |
--enable-dropout |
Enable dropout |
--disable-dropout |
Disable dropout |
| Query Type | Description |
|---|---|
input-size |
Get input layer size |
output-size |
Get output layer size |
hidden-size |
Get hidden layer size (requires --layer) |
cell-type |
Get cell type (simplernn/lstm/gru) |
sequence-length |
Get current sequence length |
dropout-rate |
Get current dropout rate |
hidden-state |
Get hidden state value (requires --layer, --timestep, --neuron) |
# Create a new model
facaded_rnn_cuda create --input=2 --hidden=16 --output=2 --cell=lstm --save=model.json
# Get model information
facaded_rnn_cuda info --model=model.json
# Query input size
facaded_rnn_cuda query --model=model.json --query-type=input-size
# Query hidden size for layer 0
facaded_rnn_cuda query --model=model.json --query-type=hidden-size --layer=0
# Query cell type
facaded_rnn_cuda query --model=model.json --query-type=cell-type
# Query hidden state at specific location
facaded_rnn_cuda query --model=model.json --query-type=hidden-state --layer=0 --timestep=0 --neuron=0
# Set dropout rate
facaded_rnn_cuda query --model=model.json --query-type=dropout-rate --dropout-rate=0.5# Run CUDA tests
./rnn_cuda_tests.sh
# Run OpenCL tests
./rnn_opencl_tests.sh
# Run C++ tests
./rnn_cpp_tests.sh
# Run Rust tests
cd rust_cuda && cargo test
cd facaded_rust_cuda && cargo testEach test suite covers:
| Category | Tests |
|---|---|
| Help & Usage | Command-line interface verification |
| Model Creation | Various architecture configurations |
| Cell Types | SimpleRNN, LSTM, GRU |
| Hyperparameters | Learning rate, activation, loss functions |
| Model Info | Metadata retrieval |
| Save & Load | Model persistence |
| Query/Introspection | Hidden state, gate values inspection |
| Error Handling | Invalid input handling |
| Cross-Implementation | API compatibility |
| Train & Predict | End-to-end workflows |
=========================================
RNN CUDA Comprehensive Test Suite
=========================================
Group: Help & Usage
Test 1: RNN help command... PASS
Test 2: RNN --help flag... PASS
Test 3: RNN -h flag... PASS
...
=========================================
Test Summary
=========================================
Total tests: 50
Passed: 50
Failed: 0
All tests passed!
The Rust Facade implementation includes Kani formal verification proofs that mathematically prove the absence of certain classes of bugs. This goes beyond traditional testing to provide mathematical guarantees about code correctness.
The test suite covers security verification categories:
| Category | Description |
|---|---|
| Strict Bound Checks | Array/collection indexing safety |
| Pointer Validity | Slice-to-pointer conversion safety |
| No-Panic Guarantee | Enum and command handling safety |
| Integer Overflow Prevention | Weight size, dimension calculations |
| Division-by-Zero Exclusion | Launch config, sequence processing |
| Global State Consistency | Training mode state tracking |
| Deadlock-Free Logic | Arc reference counting |
| Input Sanitization Bounds | Loop iteration limits |
| Result Coverage Audit | Error handling completeness |
| Memory Leak Prevention | Vector allocation bounds |
| Constant-Time Execution | Timing-safe operations |
| State Machine Integrity | Training state transitions |
| Enum Exhaustion | Match statement completeness |
| Floating-Point Sanity | NaN/Infinity prevention |
| Resource Limit Compliance | Memory budget enforcement |
# Facade RNN
cd facaded_rust_cuda
cargo kani
# Run specific proof
cargo kani --harness verify_hidden_indexingTraditional testing can only verify specific test cases. Formal verification with Kani:
- Exhaustively checks all possible inputs within defined bounds
- Mathematically proves absence of panics, buffer overflows, and undefined behavior
- Catches edge cases that random testing might miss
- Provides cryptographic-level assurance for safety-critical code
This project follows CISA (Cybersecurity and Infrastructure Security Agency) and NSA (National Security Agency) Secure by Design principles:
| Principle | Implementation |
|---|---|
| Memory Safety | Rust ownership model eliminates buffer overflows, use-after-free, and data races |
| Formal Verification | Kani proofs mathematically verify absence of critical bugs |
| Input Validation | All CLI inputs validated before processing |
| Defense in Depth | Multiple layers of safety (language, compiler, runtime checks) |
| Secure Defaults | Safe default configurations throughout |
| Transparency | Open source with full code visibility |
- Memory-safe language (Rust implementation)
- Static analysis (Rust compiler + Clippy)
- Formal verification (Kani proof harnesses)
- Comprehensive testing (Unit tests + integration tests)
- Bounds checking (Verified array access)
- Input validation (CLI argument parsing)
- No unsafe code in critical paths (Where possible)
- Documentation (Inline docs + README)
- Version control (Git)
- License clarity (MIT License)
This codebase has been developed following secure software development lifecycle (SSDLC) practices and demonstrates:
- Formal verification proofs passed (Kani proofs)
- Zero warnings compilation across all implementations
- Consistent API across all language/backend combinations
- Production-ready code quality
MIT License
Copyright (c) 2025 Matthew Abbott
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
Matthew Abbott
Email: mattbachg@gmail.com
Built with precision. Verified with rigor. Secured by design.