LLVM & AIMS Verification Tooling
12 sections
87%
Section 1 Verifier Gates & Quick Wins Section 2 Shared Test Harness Infrastructure Section 3 AIMS Pass-Level Snapshot Tests Section 4 AIMS Lattice Property Verification Section 5 Contract Coherence Oracle Section 6 Protocol Builtin Verification Matrix Section 7 FileCheck-Style IR Pattern Matching Section 8 Sanitizer Integration Section 9 Alive2 Formal Verification Section 10 Differential Oracle Fuzzing Section 11 CI Integration & ARC IR Parity Section 12 Verification Dashboard & Regression Tracking
Overview
Build world-class verification tooling for Ori's AIMS memory system and LLVM backend — exploiting Ori's unique dual-layer architecture (ARC IR + LLVM IR + Interpreter differential oracle) to create verification capabilities that exceed what Rust, Swift, Lean4, or Koka have. Make verification failures blocking gates in test/CI, not informational warnings. The AIMS pipeline's 7-dimensional product lattice, 12-step observable pipeline, and contract-realization coherence requirements demand purpose-built tooling that no other compiler needs — because no other compiler has this architecture.
Completed
9 sections
Section 1 Complete
Verifier Gates & Quick Wins
112/112 tasks
112/112 tasks
Section 2 Complete
Shared Test Harness Infrastructure
120/120 tasks
120/120 tasks
Section 3 Complete
AIMS Pass-Level Snapshot Tests
84/84 tasks
84/84 tasks
Section 4 Complete
AIMS Lattice Property Verification
93/93 tasks
93/93 tasks
Section 5 Complete
Contract Coherence Oracle
85/85 tasks
85/85 tasks
Section 6 Complete
Protocol Builtin Verification Matrix
54/54 tasks
54/54 tasks
Section 7 Complete
FileCheck-Style IR Pattern Matching
103/103 tasks
103/103 tasks
Section 8 Complete
Sanitizer Integration
161/161 tasks
161/161 tasks
Section 9 Complete
Alive2 Formal Verification
108/108 tasks
108/108 tasks