Skip to main content
BRIK-64

​
BRIK-64 — Digital Circuitality

Digital Circuitality is the formal property of a computational system that operates as a closed circuit: every input domain is bounded, every operation is verified, every output range is proven, and no external noise can introduce undefined behavior. A system with Φ_c = 1 satisfies Digital Circuitality. A system with Φ_c = 0 does not. BRIK-64 is the first programming system built entirely on this principle — and the only one where a program that cannot be certified cannot compile.

64 Certified Monomers

MC_00–MC_63: atomic verified operations with Coq proofs. Φ_c = 1 guaranteed. The foundation.

64 Extended Monomers

MC_64–MC_127: float, network, graphics, audio, concurrency, FFI. Not certified — but formally bounded. BRIK-64 Open.

EVA Algebra

⊗ sequential · ∥ parallel · ⊕ conditional. Correctness preserved by composition. Proven in Coq.

TCE Certification

Thermodynamic Coherence Engine. Φ_c = 1 · ΔN = 0 · Cₘ = 1. The compiler rejects everything else.

​
What BRIK-64 Gives You

​
Write PCD, compile to any target

PCD (Printed Circuit Description) is the language of Digital Circuitality — a formal schematic language, not a scripting language. Write once, compile to five targets: 
brikc compile src/main.pcd              # Native x86-64 ELF — standalone, no libc
brikc compile src/main.pcd --target rs  # Idiomatic Rust
brikc compile src/main.pcd --target js  # JavaScript ES2022
brikc compile src/main.pcd --target py  # Python 3.10+
brikc compile src/main.pcd --target wasm32  # WebAssembly
The guarantees travel with the output. A certified PCD program compiles to certified Rust, certified JavaScript, certified Python — no BRIK-64 runtime required at the destination.

​
Use BRIK-64 in your existing codebase

Apply Digital Circuitality principles inside Rust, Python, or JavaScript without rewriting anything: 
use brik64::{mc, eva};
let result = eva::seq(mc::add8(a, b), mc::mod8(x, n));
// Φ_c = 1 — this composition is formally verified

from brik64 import mc, eva
result = eva.seq(mc.add8(a, b), mc.mod8(x, n))

import { mc, eva } from '@brik64/core';
const result = eva.seq(mc.add8(a, b), mc.mod8(x, n));
Any function built from Core monomers (MC_00–MC_63) via EVA operators retains Φ_c = 1 — regardless of which language it runs in.

​
The Two Monomer Tiers

​
Core: MC_00–MC_63 — BRIK-64 Certified

64 formally verified atomic operations, 8 families × 8. Every monomer has a Coq proof covering domain, range, postconditions, and termination.
FamilyRangeOperations
ArithmeticMC_00–07ADD8, SUB8, MUL8, DIV8, INC, DEC, MOD, NEG
LogicMC_08–15AND8, OR8, XOR8, NOT8, SHL, SHR, ROTL, ROTR
MemoryMC_16–23LOAD, STORE, ALLOC, FREE, COPY, SWAP, CAS, FENCE
ControlMC_24–31IF, JUMP, CALL, RET, LOOP, BREAK, CONT, HALT
I/OMC_32–39READ, WRITE, OPEN, CLOSE, SEEK, STAT, POLL, FLUSH
StringMC_40–47CONCAT, SPLIT, SUBSTR, LEN, UPPER, CHAR_AT, TRIM, MATCH
CryptoMC_48–55HASH, HMAC, AES_ENC, AES_DEC, SHA256, RAND, SIGN, VERIFY
SystemMC_56–63TIME, SLEEP, ENV, EXIT, PID, SIGNAL, MMAP, SYSINFO
A program built exclusively from Core monomers receives the BRIK-64 Certified badge (Ω = 1). The compiler rejects it if Φ_c ≠ 1, ΔN ≠ 0, or Cₘ ≠ 1. There is no partial credit.

​
Extended: MC_64–MC_127 — BRIK-64 Open

64 additional monomers for real-world I/O, floating point, networking, graphics, audio, concurrency, and foreign interop. They operate under declared contracts, not formal proofs.
FamilyRangeDomain
Float64MC_64–71IEEE 754 — FADD, FSUB, FMUL, FDIV, FSQRT, FABS, FCONV, FCMP
MathMC_72–79SIN, COS, TAN, ATAN2, LOG, EXP, POW, FLOOR
NetworkMC_80–87TCP_CONN, TCP_SEND, TCP_RECV, UDP_SEND, DNS, HTTP_GET, HTTP_POST, TLS
GraphicsMC_88–95FB_INIT, FB_PIXEL, FB_LINE, FB_RECT, FB_BLIT, FB_FLIP, FB_TEXT, FB_CLOSE
AudioMC_96–103AU_INIT, AU_PLAY, AU_STOP, AU_MIX, AU_VOL, AU_SEEK, AU_STREAM, AU_CLOSE
Filesystem+MC_104–111DIR_LIST, DIR_CREATE, DIR_DELETE, CHMOD, CHOWN, LINK, WATCH, TEMP
ConcurrencyMC_112–119SPAWN, JOIN, CHAN_NEW, CHAN_SEND, CHAN_RECV, MUTEX, ATOMIC, YIELD
Interop/FFIMC_120–127FFI_LOAD, FFI_CALL, FFI_ALLOC, FFI_FREE, WASM_EXEC, PY_EVAL, JSON_PARSE, JSON_EMIT
Programs mixing Core + Extended compile with --open and receive the BRIK-64 Open badge showing the verified percentage. Extended monomers must be leaves of the computation graph — the main data flow must pass through Core before OUTPUT.
Critical invariant: Core monomers (MC_00–MC_63) remain formally verified regardless of what Extended monomers surround them. The compiler enforces the boundary statically. Extended results entering Core logic must pass a typed validation boundary.

​
Certification

Every certified program produces a cryptographic certificate: 
{
  "tce": { "phi_c": 1.000, "delta_n": 0.000, "c_m": 1.000, "omega": 1 },
  "badge_type": "certified",
  "public_hash": "sha256:7229cf...",
  "merkle_proof": { "chain": "arbitrum", "block": 8823421 }
}
The badge in your README is a live endpoint — it verifies the certificate hash against the public registry in real time. A modified program shows INVALID automatically.
BadgeConditionMeaning
🟢 BRIK-64 CERTIFIED100% Core, Ω = 1Structurally impossible to have logic errors
🔵 BRIK-64 OPEN 78%Core + ExtendedCertified where Core, contracted at the boundary
⚫ UNVERIFIEDNot in registryNo claim made
What no other certification standard can claim:
StandardWhat it certifies
ISO 26262, DO-178C, CC EAL7The process was followed / the tests were run
BRIK-64 CertifiedIncorrect programs cannot compile

​
The Thermodynamic Foundation

BRIK-64 connects computation to physics (Paper II). Every irreversible bit operation dissipates a minimum of k_B · T · ln(2) ≈ 2.87 × 10⁻²¹ J at room temperature — the Landauer Limit. The ΔN metric measures the Landauer Gap: how far your program operates above the thermodynamic minimum. A certified program with ΔN = 0 closes the gap entirely. Its only remaining failure mode is hardware — modern silicon fails at approximately 10⁻¹⁹ per operation. Logic errors, type errors, integer overflow, and undefined behavior are not rare events in a certified BRIK-64 program. They are structurally impossible.

​
Quick Start

# Install (Linux x86-64)
curl -L https://brik64.dev/install | sh

# Verify
brikc version
brikc verify
brikc catalog   # list all 128 monomers

PC hello {
    let msg = "Hello from Digital Circuitality!";
    let n = MC_43.LEN(msg);
    MC_58.WRITE(1, msg, n);
    OUTPUT 0;
}

brikc compile hello.pcd   # Φ_c = 1 — or it doesn't compile

Quickstart

Get running in 5 minutes

PCD Language

Write your first circuit

Formal Theory

Landauer, Φ_c, Ω = 1