Skip to main content

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 compilerbrikc compiles itself, fixpoint hash 7229cfcde9...
  • 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
  • CLIbrikc 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):
  1. Compiles only if Φ_c = 1, ΔN = 0, Cₘ = 1 — the compiler rejects otherwise
  2. Produces a certificate.json with a cryptographic signature
  3. Can be verified locally: brikc cert verify certificate.json
  4. Operates at the Landauer thermodynamic boundary — ΔN = 0 means zero logical noise
The certified program cannot have logic errors. Not “probably won’t” — structurally cannot. The compiler is the proof.

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:
FamilyRangeNamePurpose
F8MC_64–71Float64IEEE 754 floating point (SSE2 native)
F9MC_72–79MathTranscendentals: sin, cos, log, exp, pow
F10MC_80–87NetworkTCP, UDP, DNS, HTTP, TLS
F11MC_88–95GraphicsFramebuffer, pixel, line, blit, text
F12MC_96–103AudioPlay, mix, stream, seek
F13MC_104–111Filesystem+Directory ops, watch, temp, chmod
F14MC_112–119ConcurrencySpawn, join, channels, mutex, atomic
F15MC_120–127Interop/FFIFFI, WASM exec, Python eval, JSON
Extended monomers operate under declared contracts, not formal proofs. The Core invariant (Φ_c = 1) is preserved for Core sections regardless of what Extended monomers surround them. BRIK-64 Open programs (mixing Core + Extended) receive a partial certification badge showing their verified percentage:
◈ BRIK-64 OPEN | 78% verified
brikc compile src/main.pcd          # Core only — rejects MC_64+
brikc compile --open src/main.pcd   # Core + Extended allowed
The boundary rule: Extended monomers must be leaves of the computation graph, not the trunk. The main data flow must pass through Core before OUTPUT. Statically verified by the TCE.

Phase 2 — Public Certification Registry (v2.1.0)

A public, append-only registry at brik64.dev/registry where every certified program is recorded. Every BRIK-64 Certified badge is a live endpoint:
[![BRIK-64 Certified](https://brik64.dev/badge/sha256:7229cf)](https://brik64.dev/cert/sha256:7229cf)
This badge makes a real-time HTTP request on every page load. If the hash is not in the registry, or has been revoked, the badge shows INVALID — automatically, without human intervention. Certificate lifecycle:
Badge colorMeaning
Green — CERTIFIEDHash registered, Ω = 1, valid
Blue — OPEN XX%Hash registered, mixed Core+Ext
Gray — UNVERIFIEDHash not in registry
Red — REVOKEDCertificate revoked
Blockchain anchoring: Every hour, the registry computes a Merkle root over all certificates and anchors it on Ethereum L2 (Arbitrum). Any certificate can be verified against the on-chain root — without trusting 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

StandardWhat it certifiesHow
ISO 26262 (automotive)The development processAudit trail
DO-178C (avionics)Test coverage was runTest logs
Common Criteria EAL7Design was reviewedExpert evaluation
SOC 2 Type IIControls were operatingAnnual audit
BRIK-64 CertifiedThe program cannot failStructural impossibility
The others certify the journey. BRIK-64 certifies the destination. CI/CD integration:
# .github/workflows/certify.yml
- name: Compile and certify
  run: brikc compile src/main.pcd

- name: Publish to registry
  run: |
    brikc cert publish \
      --token ${{ secrets.BRIK64_API_KEY }} \
      --version ${{ github.ref_name }}
  # Fails here if Ω ≠ 1 — blocks the release

Phase 3 — BPU Silicon (Future)

The BRIK Processing Unit is a hardware coprocessor implementing the 64 Core monomers directly in silicon:
┌─────────────────────────────────────────┐
│              BPU Chip                   │
│                                         │
│  ┌─────────────────────────────────┐   │
│  │  64 Core Monomer Units          │   │  ← Silicon, formally verified
│  │  (MC_00 – MC_63)                │   │
│  ├─────────────────────────────────┤   │
│  │  EVA Router                     │   │  ← Composition logic in hardware
│  ├─────────────────────────────────┤   │
│  │  TCE Unit (Φ_c checker)         │   │  ← Coherence verification in hardware
│  └─────────────────────────────────┘   │
│                                         │
│  Policy evaluation:                     │
│  action → PCD circuit → ALLOW / BLOCK  │
│  Non-maskable. Cannot be overridden.   │
│                                         │
└─────────────────────────────────────────┘
The BPU evaluates Policy Circuits — PCD programs (Core only) that verify AI actions before execution. The evaluation happens in hardware. The BLOCK is non-maskable. Software cannot override it. This is the difference between teaching an AI to want to do right (RLHF) and preventing it from doing wrong (physics). Education fails. Physics does not. The regulatory trajectory:
2026:  Voluntary — early adopters use BPU for safety-critical AI
2028:  Industry standard — major AI labs adopt Policy Circuits
2030:  Mandatory — regulators require hardware-enforced AI safety
       (precedent: ABS was voluntary in 1978, mandatory in 2004)
The BPU is licensed under an ARM-style model — chip manufacturers pay per unit. The architecture is published; the manufacturing rights are licensed.

The Expansion at a Glance

PhaseVersionDeliverableStatus
Core self-hostingv2.0.0Compiler compiles itself, fixpoint verifiedComplete
BRIK-64 Openv2.5.064 Extended monomers, partial certificationRoadmap
Registry + Badgesv2.1.0Public registry, live badges, blockchain anchoringRoadmap
BIR runtimev3.0.0Portable execution on any platformRoadmap
BPU simulatorv3.5.0Software-emulated BPU for policy developmentRoadmap
BPU siliconv4.0.0Hardware coprocessor, ARM-style licensingRoadmap

Prior Art & Publications

Before infrastructure: the prior art must be registered.
  1. Zenodo — permanent DOI for compiler v2.0.0 + fixpoint hash 7229cf...
  2. USPTO — 5 provisional patents, 12-month priority window
  3. arXiv — Paper cs.PL + cs.AI + cs.AR covering Digital Circuitality framework
  4. Software Heritage — permanent archive of the source tree
The hash is the prior art. The badge is the business. The patent is the moat.