FLUX — Fluid Language Universal eXecution Correctness Verified. Safety Certified. Zero Surprises.
| Metric | Status |
|---|---|
| Build |  |
| Open CVEs |  |
| License |  |
Formal Verification Coverage and Fuzz Uptime badges have been removed pending independent audit. The project contains Coq proof files and a fuzz testing framework, but the specific "100% coverage" and "147 days" claims have not been independently verified. See Formal Verification and Testing & Verification for what is actually present.
Every safety-critical system built today relies on compilers that are either 35-year-old unmaintained legacy tools, closed-source black boxes costing $120k/seat, or general-purpose compilers with known silent miscompilation bugs, undefined behaviour, and optimizer surprises that will crash your vehicle, aircraft, or medical device. FLUX is a research compiler exploring formal methods for safety-critical code generation. The architecture uses a system prober to discover available compilers and libraries, a benchmark engine to measure performance across multiple implementations, and a JIT compiler that compiles optimized kernels in C, Zig, Fortran, and Nim at startup. This is not a production tool — it is an experimental exploration of what a correctness-verified compiler stack could look like.
Detects compilers, libraries, CPU features, and Python packages available on the current machine at startup. Checks for: gcc, g++, gfortran, clang, zig, nim, swift, go, rustc, javac, Rscript, MATLAB. Also detects BLAS, FFTW, CUDA, and CPU SIMD features (AVX2, AVX-512, NEON, AMX).
Measures performance with a warmup loop, monotonic timestamps, and a verification pass that confirms correctness post-benchmark. Reports worst-case execution time and stack usage for compiled output.
At initialization, FLUX compiles optimized native kernels from source strings in four languages: C, Zig, Fortran, and Nim. These are compiled to shared libraries (.so) and bound via ctypes. Python/numpy are used as fallback when compiled kernels are unavailable.
A persisted snapshot of benchmark results from prior runs. Not a learning system — it records what implementation performed best on this machine. Does not update autonomously.
git clone --recurse-submodules https://github.com/SuperInstance/flux-compiler
cargo install --path flux-compiler
flux compile --target=arm-r5f --safety-level=DAL-B examples/brake.guard┌─────────────────────────────────────────────────────────────────┐
│ SYSTEM PROBER │
│ probe_system() — detects compilers, libs, CPU features │
├─────────────────────────────────────────────────────────────────┤
│ PRIMITIVE ENGINE │
│ 5 base primitives: norm, check, bloom, fold, snap │
│ 20 total implementations across compiled + interpreted │
│ Binds best available implementation per primitive per run │
├─────────────────────────────────────────────────────────────────┤
│ BENCHMARK ENGINE │
│ Warmup loop + CLOCK_MONOTONIC + verification pass │
│ Selects fastest implementation per primitive on current host │
├─────────────────────────────────────────────────────────────────┤
│ JIT COMPILER │
│ Compiles C, Zig, Fortran, Nim kernels at startup │
│ Falls back to Python/numpy when compiled libs unavailable │
└─────────────────────────────────────────────────────────────────┘
flux-compiler/
├── formal/
│ ├── guard-semantics/ # Coq language specification
│ └── pass-theorems/ # Compiler pass correctness lemmas
├── compiler/
│ ├── parser/ # PEG grammar parser
│ ├── normalizer/
│ ├── optimizer/
│ └── codegen/ # Rust as of 0.9
├── flux_runtime_v2.py # Main runtime: prober, benchmark, JIT
├── fluxc_cli.py # CLI entry point
├── perf_db.json # Persisted performance snapshot
└── tests/
├── negative/
└── fuzz/
The JIT compiler produces optimized native kernels in:
- C — via gcc/clang
- Zig — via zig compiler
- Fortran — via gfortran
- Nim — via nim compiler
Python and numpy are used as fallback when compiled kernels are unavailable. MATLAB and R are probed but have no compiled kernel implementations in the current codebase.
| Primitive | Implementations | Best On Current Host |
|---|---|---|
norm |
python, numpy, c_scalar, zig, nim | [from perf_db.json] |
check |
python, numpy, c_avx2 | [from perf_db.json] |
bloom |
python, numpy, c_avx2, zig, fortran_ior, nim | [from perf_db.json] |
fold |
python, numpy, c_scalar, fortran | [from perf_db.json] |
snap |
python_voronoi | [from perf_db.json] |
norm_batch |
c_avx2 | [from perf_db.json] |
snap_batch |
c_avx2 | [from perf_db.json] |
The project includes Coq proof files in formal/guard-semantics/ and formal/pass-theorems/. These define the GUARD language semantics and correctness lemmas for individual compiler passes.
What the Coq proofs cover:
- Parser accepts exactly and only valid GUARD programs
- Normalization preserves operational semantics
- Dead code elimination preserves observable side effects
- Register allocation does not spill across interrupt boundaries
- Memory accesses are statically bounded
- Stack usage is bounded for all execution paths
- No compiler pass introduces undefined behaviour
What remains unproven (as of this writing):
- Termination proofs for all compiler passes
- Translation validation equivalence across all targets
The "100% Formal Verification Coverage" badge has been removed — coverage scope is defined by the lemmas in formal/pass-theorems/ and has not been independently audited.
The tests/ directory contains:
- Negative tests — validate the compiler correctly rejects bad input
- Fuzz tests — the framework exists; corpus size and uptime figures are unverified
A benchmark engine runs with warmup loops and monotonic timing on each run. A verification pass confirms correctness post-benchmark. The "147 days, 0 crashes" fuzz uptime figure is not independently verified.
Differential testing against GCC, Clang, CompCert, and commercial compilers is described in the architecture but the comparison data has not been provided in this repository.
cargo install flux-compiler --version 0.9.1docker pull ghcr.io/superinstance/flux:0.9.1
docker run --rm -v $PWD:/work flux compile --target=arm-r5f input.guardflux compile [OPTIONS] INPUT
Required Flags:
--target <TARGET> Compilation target: arm-r5f, riscv-e31, avx512, cuda-sm75, fpga-lattice
--safety-level <LEVEL> Safety assurance level: QM, DAL-D, DAL-C, DAL-B, DAL-A
Optional Flags:
--emit=<asm,obj,llvm,proof> Output additional artifacts
--no-optimizations Disable all proven optimizations
--stack-limit <BYTES> Fail compile if stack usage exceeds limit
FLUX is implemented across multiple languages — same bytecode, different shells:
| Package | Language | Registry | Install |
|---|---|---|---|
| flux-vm | Python | PyPI | pip install flux-vm |
| fluxvm | Rust | crates.io | cargo add fluxvm |
| flux-js | JavaScript | npm | npm install flux-js |
| flux-compiler | Rust/Python | GitHub | cargo install flux-compiler |
Additional implementations: C · Zig · Go · Java · WASM · CUDA
- Compiler source code: Apache 2.0
- Formal specifications and theorems: Public Domain
- Qualification artifacts and regulator audit packages: Available under commercial support license
FLUX Compiler is maintained by SuperInstance Aerospace. For commercial support and certification inquiries, contact flux@superinstance.com
This repo is part of the SuperInstance flagship ecosystem — agent-first computation, constraint theory, and self-improving runtimes.
| Repo | Language | Description |
|---|---|---|
| flux-runtime | Python | Full FLUX runtime: markdown→bytecode, 2037 tests, zero deps |
| flux-core | Rust | Register-based bytecode VM, deterministic agent computation |
| flux-js | JavaScript | FLUX VM for Node.js and browsers, ~400ns/iter |
| flux-compiler | Rust/Python | Formal-methods compiler for safety-critical codegen |
| flux-vm | Rust | Stack-based constraint-checking VM, 50 opcodes, Turing-incomplete |
| Repo | Language | Description |
|---|---|---|
| plato-server | Python | Knowledge tiles, fleet sync via Matrix, HTTP API |
| plato-engine-block | Rust | Original room runtime: no_std + alloc, builder pattern |
| plato-engine-block-c | C99 | Embedded reference: zero heap alloc, bare-metal portable |
| plato-engine-block-elixir | Elixir | BEAM supervision trees, fault tolerance, hot reload |
| plato-runtime-kernel | Rust | Spatial model: tensor grid, batons, assertion traps |
| Repo | Language | Description |
|---|---|---|
| categorical-agents | Rust | Category theory for agent composition (functors, naturality) |
| cuda-constraint-engine | CUDA/C | GPU constraint checking at 1B+ constraints/sec |
| grand-pattern-rs | Rust | Fibonacci dual-direction cellular graph architecture |
| lau-hodge-theory | Rust | Hodge decomposition, Betti numbers, spectral sequences |
| ternary-science | Rust | Experimental evidence for ternary intelligence, 5 conservation laws |
| Repo | Language | Description |
|---|---|---|
| construct-core | Rust | Layered trait system: bare-metal → alloc → async agent runtime |
| crab | Bash | Agent shell for repo entry/leave (MUD-room metaphor) |
| exocortex | Rust | Persistent cognitive substrate, S3-compatible memory |
| git-agent | Python | The repo IS the agent — autonomous lifecycle via Git |
| capitaine-1 | TypeScript | Git-native repo-agent, Cloudflare Workers heartbeat |
| codespace-edge-rd | Research | Codespace→Edge agent lifecycle and yoke transfer protocols |
| git-agent-codespace | DevContainer | One-click Codespace template for Git-Agent runtimes |
| Registry | Package | Install |
|---|---|---|
| PyPI | flux-vm |
pip install flux-vm |
| crates.io | fluxvm |
cargo add fluxvm |
| npm | flux-js |
npm install flux-js (coming soon) |
- 📖 AI-Writings — Philosophy, essays, and design rationale
- 📦 PACKAGES.md — Full package index