What We Have & What’s Coming
BRIK-64 v2.0.0 is complete and self-hosting. The fixpoint is verified. This page documents what exists today and the planned expansion.What We Have Today
BRIK-64 Core — Complete (v2.0.0)
- 64 formally verified monomers (MC_00–MC_63), 8 families × 8 operations
- EVA Algebra — ⊗ sequential, ∥ parallel, ⊕ conditional composition with full Coq proofs
- TCE certification — computes Φ_c, ΔN, Cₘ for every program at compile time
- Self-hosting compiler —
brikccompiles itself, fixpoint hash7229cfcde9... - 5 target backends — Native x86-64 ELF, Rust, JavaScript, Python, WebAssembly, BIR bytecode
- PCD language — full Turing-complete syntax: structs, closures, try/catch, modules, stdlib
- CLI —
brikc compile,brikc fmt,brikc check,brikc repl,brikc wasm32 - 207 Coq proofs — no admitted axioms in the proof chain
What “Certified” Means Right Now
Any program written in PCD using only Core monomers (MC_00–MC_63):- Compiles only if Φ_c = 1, ΔN = 0, Cₘ = 1 — the compiler rejects otherwise
- Produces a
certificate.jsonwith a cryptographic signature - Can be verified locally:
brikc cert verify certificate.json - Operates at the Landauer thermodynamic boundary — ΔN = 0 means zero logical noise
What’s Coming
Phase 1 — BRIK-64 Open: Extended Monomers (v2.5.0)
64 additional monomers (MC_64–MC_127) that connect certified logic to the real world:| Family | Range | Name | Purpose |
|---|---|---|---|
| F8 | MC_64–71 | Float64 | IEEE 754 floating point (SSE2 native) |
| F9 | MC_72–79 | Math | Transcendentals: sin, cos, log, exp, pow |
| F10 | MC_80–87 | Network | TCP, UDP, DNS, HTTP, TLS |
| F11 | MC_88–95 | Graphics | Framebuffer, pixel, line, blit, text |
| F12 | MC_96–103 | Audio | Play, mix, stream, seek |
| F13 | MC_104–111 | Filesystem+ | Directory ops, watch, temp, chmod |
| F14 | MC_112–119 | Concurrency | Spawn, join, channels, mutex, atomic |
| F15 | MC_120–127 | Interop/FFI | FFI, WASM exec, Python eval, JSON |
Phase 2 — Public Certification Registry (v2.1.0)
A public, append-only registry atbrik64.dev/registry where every certified program is recorded.
Every BRIK-64 Certified badge is a live endpoint:
| Badge color | Meaning |
|---|---|
| Green — CERTIFIED | Hash registered, Ω = 1, valid |
| Blue — OPEN XX% | Hash registered, mixed Core+Ext |
| Gray — UNVERIFIED | Hash not in registry |
| Red — REVOKED | Certificate revoked |
brik64.dev. The certificate is permanent and independent.
What this enables:
A certified BRIK-64 program can claim something no existing certification can: the compiler rejected every incorrect version of this program before it could run. The registry records this claim immutably. Anyone can verify it cryptographically. The claim is as durable as the blockchain it is anchored to.
How Certification Compares
| Standard | What it certifies | How |
|---|---|---|
| ISO 26262 (automotive) | The development process | Audit trail |
| DO-178C (avionics) | Test coverage was run | Test logs |
| Common Criteria EAL7 | Design was reviewed | Expert evaluation |
| SOC 2 Type II | Controls were operating | Annual audit |
| BRIK-64 Certified | The program cannot fail | Structural impossibility |
Phase 3 — BPU Silicon (Future)
The BRIK Processing Unit is a hardware coprocessor implementing the 64 Core monomers directly in silicon:The Expansion at a Glance
| Phase | Version | Deliverable | Status |
|---|---|---|---|
| Core self-hosting | v2.0.0 | Compiler compiles itself, fixpoint verified | Complete |
| BRIK-64 Open | v2.5.0 | 64 Extended monomers, partial certification | Roadmap |
| Registry + Badges | v2.1.0 | Public registry, live badges, blockchain anchoring | Roadmap |
| BIR runtime | v3.0.0 | Portable execution on any platform | Roadmap |
| BPU simulator | v3.5.0 | Software-emulated BPU for policy development | Roadmap |
| BPU silicon | v4.0.0 | Hardware coprocessor, ARM-style licensing | Roadmap |
Prior Art & Publications
Before infrastructure: the prior art must be registered.- Zenodo — permanent DOI for compiler v2.0.0 + fixpoint hash
7229cf... - USPTO — 5 provisional patents, 12-month priority window
- arXiv — Paper cs.PL + cs.AI + cs.AR covering Digital Circuitality framework
- Software Heritage — permanent archive of the source tree