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.

128 Hardened Monomers

MC_00–MC_63 (Coq-proven) + MC_64–MC_127 (contracted). 0 panic guarantee on all 128. 14,500+ tests across 16 suites.

EVA Algebra

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

CMF Certification

Coherence Metric Framework. Φ_c = 1 · δ = 0 · V(C) = 1. The compiler rejects everything else.

Roadmap

Extended Monomers · Certification Registry · BPU Silicon. The path from software to hardware.

Your compiled code ships with its test suite

Every team knows the pain: code is done, but tests aren’t. Or tests pass, but someone changed the logic later and they didn’t catch it. BRIK-64 changes this at the compiler level.

brikc compile src/main.pcd --target rs --emit-tests
# build/main.rs          ← certified implementation
# build/main_spec.rs     ← complete test suite, auto-generated from the proof

The test suite is generated from the formal proof — not written by hand. Property tests, boundary tests, composition tests, and regression anchors arrive alongside the code. Your CI pipeline gets:

✅ Correct code — proven by CMF, not hoped by coverage
✅ Complete test suite — generated, not maintained
✅ Regression anchors — if anyone changes the generated code, tests catch the deviation

The compiler does not just verify your logic. It also documents and protects it. → Testing & Debugging

Use BRIK-64 Now — In Any Language

You do not need to switch languages to apply Digital Circuitality. BRIK-64 ships native libraries for Rust, JavaScript/TypeScript, and Python. Drop them into your existing codebase and any function built from Core monomers via EVA operators automatically carries Φ_c = 1.

Install

Rust
JavaScript / TypeScript
Python
PCD Compiler

cargo add brik64-core

Or in Cargo.toml:

[dependencies]
brik64-core = "4.1.0-beta.1"

Usage:

use brik64_core::{mc, eva};

fn main() {
    // Wrapping 8-bit addition — formally verified
    let result = mc::add8(200, 100); // → 44 (wrapping: (200+100) % 256)

    // EVA sequential composition: add8 then mod8
    let pipeline = eva::seq(|x: (u8,u8)| mc::add8(x.0, x.1), |s| mc::mod8(s, 7));
    println!("{}", pipeline((250, 10))); // Φ_c = 1 for the entire composition
}

Available crates:

brik64-core — 64 core monomers + EVA algebra
brik64-bir — BIR bytecode interpreter

npm install @brik64/core
# or
yarn add @brik64/core
# or
pnpm add @brik64/core

Usage (TypeScript):

import { mc, eva } from '@brik64/core';

// Wrapping 8-bit addition
const result = mc.add8(200, 100); // → 44 (wrapping)

// EVA sequential composition
const pipeline = eva.seq(
  (x: number) => mc.add8(x, 10),
  (x: number) => mc.mod8(x, 7)
);

console.log(pipeline(250)); // Φ_c = 1

Usage (CommonJS):

const { mc, eva } = require('@brik64/core');

const result = mc.add8(200, 100); // 44 (wrapping)
const hash = mc.hashHex(Buffer.from('hello')); // SHA-256 hex

Full tree-shakeable ESM + CJS dual build. TypeScript types included.

pip install brik64
# or
uv add brik64

Usage:

from brik64.mc import arithmetic, crypto
from brik64.eva import seq, par, pipeline

# Wrapping 8-bit addition
result = arithmetic.add8(200, 100)  # → 44 (wrapping)

# EVA sequential composition
process = seq(
    lambda x: arithmetic.add8(x, 10),
    lambda x: arithmetic.mod8(x, 7)
)
print(process(250))  # Φ_c = 1

# SHA-256 hash (MC_49)
digest = crypto.hash_hex(b"hello world")

Requires Python 3.10+. Zero dependencies.

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

# Verify installation
brikc version
brikc verify           # self-verification: Ω = 1
brikc catalog          # list all 128 monomers

The brikc compiler is itself a certified BRIK-64 program. It compiles to a 708 KB standalone x86-64 ELF — no Rust runtime, no libc dependency.

# Compile PCD to native ELF
brikc compile src/main.pcd

# Cross-compile to other targets
brikc compile src/main.pcd --target rs    # 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

What Φ_c = 1 means in practice

When you call add8(200, 100) instead of 200 + 100 in any language, you are not just using a utility function. You are invoking a formally verified operation whose entire domain and range have been proven in Coq. The EVA operators (seq, par, cond) preserve that proof across composition. Any function built exclusively from Core monomers (MC_00–MC_63) via EVA operators retains Φ_c = 1 — regardless of which language it runs in. That is the definition of Digital Circuitality.

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 14 targets (JS, TypeScript, Python, Rust, C, C++, Go, COBOL, PHP, Java, Swift, WASM, Native). Lift from 10 input languages with 100% liftability on real projects:

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

brikc compile hello.pcd               # Φ_c = 1 — or it doesn't compile
brikc compile hello.pcd --target rs   # emit Rust
brikc compile hello.pcd --target js   # emit JavaScript
brikc compile hello.pcd --target py   # emit Python

The guarantees travel with the output. A certified PCD program compiles to certified Rust, certified JavaScript, certified Python — the BRIK-64 runtime is not required at the destination.

The Core Monomer Catalog — MC_00–MC_63

64 formally verified atomic operations, 8 families × 8. Every monomer has a Coq proof covering domain, range, postconditions, and termination.

Family	Range	Operations
Arithmetic	MC_00–07	ADD8, SUB8, MUL8, DIV8, INC, DEC, MOD, NEG
Logic	MC_08–15	AND8, OR8, XOR8, NOT8, SHL, SHR, ROTL, ROTR
Memory	MC_16–23	LOAD, STORE, ALLOC, FREE, COPY, SWAP, CAS, FENCE
Control	MC_24–31	IF, JUMP, CALL, RET, LOOP, BREAK, CONT, HALT
I/O	MC_32–39	READ, WRITE, OPEN, CLOSE, SEEK, STAT, POLL, FLUSH
String	MC_40–47	CONCAT, SPLIT, SUBSTR, LEN, UPPER, CHAR_AT, TRIM, MATCH
Crypto	MC_48–55	HASH, HMAC, AES_ENC, AES_DEC, SHA256, RAND, SIGN, VERIFY
System	MC_56–63	TIME, 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, δ ≠ 0, or V(C) ≠ 1. There is no partial credit.

Extended Monomers — MC_64–MC_127

Available since v4.0.0-beta.2. Extended monomers (MC_64–MC_127) cover floating point, math, networking, graphics, audio, filesystem, concurrency, and interop. All 64 are implemented with bounds-checked input validation — 0 panic paths. They operate under CONTRACT closure (Φ_c = CONTRACT) rather than the Coq-proven Φ_c = 1 of Core monomers.

64 additional monomers for real-world I/O — all bounds-checked with 0 panic guarantee since v4.1.0-beta.1. They operate under declared contracts, not formal Coq proofs. Programs mixing Core + Extended receive the BRIK-64 Open badge showing the verified percentage.

Family	Range	Domain	Status
Float64	MC_64–71	IEEE 754 — FADD, FSUB, FMUL, FDIV, FABS, FNEG, FSQRT, FMOD	✅ Real implementation
Math	MC_72–79	SIN, COS, TAN, EXP, LN, LOG2, POW, CEIL	✅ Real implementation
Network	MC_80–87	CONN, SEND, RECV, CLOSE, BIND, LISTEN, ACCEPT, POLL	✅ Bounds-checked (returns DomainViolation)
Graphics	MC_88–95	CREATE, PIXEL, READ, CLEAR, BLIT, LINE, RECT, DIMS	✅ Bounds-checked (returns DomainViolation)
Audio	MC_96–103	CREATE, WRITE, READ, MIX, GAIN, LEN, RATE, CHANS	✅ Bounds-checked (returns DomainViolation)
Filesystem	MC_104–111	STAT, MKDIR, RMDIR, LIST, COPY, RENAME, REMOVE, EXISTS	✅ Bounds-checked (returns DomainViolation)
Concurrency	MC_112–119	SPAWN, JOIN, MUTEX, LOCK, UNLOCK, CHAN, SEND, RECV	✅ Bounds-checked (returns DomainViolation)
Interop	MC_120–127	CALL, LOAD, FREE, JSON_E, JSON_D, WASM_L, WASM_C, WASM_F	✅ Bounds-checked (returns DomainViolation)

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:

{
  "cmf": { "phi_c": 1.000, "delta": 0.000, "v_c": 1, "omega": 1 },
  "badge_type": "certified",
  "public_hash": "sha256:beb2c1c6634b...",
  "merkle_proof": { "registry": "registry.brik64.dev", "certified": true }
}

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.

Badge	Condition	Meaning
🟢 BRIK-64 CERTIFIED	Hash in registry, Ω = 1	Structurally impossible to have logic errors
🔵 BRIK-64 OPEN 78%	Hash in registry, Core + Extended	Certified where Core, contracted at the boundary
⚫ UNVERIFIED	Hash not in registry	No certification claim made
🔴 INVALID	Hash mismatch — code modified after certification	The program no longer matches the certified version
🔴 REVOKED	Certificate explicitly revoked	Withdrawn from registry

The badge is a live endpoint — on every page load it queries the registry with the program’s hash. If the deployed binary differs from the certified one by a single byte, the badge immediately turns red and shows INVALID. No manual audit. No delayed detection. The tamper signal is automatic and instant. What no other certification standard can claim:

Standard	What it certifies
ISO 26262, DO-178C, CC EAL7	The process was followed / the tests were run
BRIK-64 Certified	Incorrect programs cannot compile

The Coherence Foundation

BRIK-64 applies a rigorous structural analysis to every program. The Coherence Metric Framework (CMF) computes 7 metrics measuring complexity, branching, type transformation, and closure — then requires Φ_c = 1.000 for compilation to succeed. A certified program with Φ_c = 1 is a closed circuit: every input is consumed, every output is produced, and every control path terminates. Logic errors, type errors, integer overflow, and undefined behavior are not rare events in a certified BRIK-64 program — they are structurally impossible.

Security Audit — v4.1.0-beta.1

All 128 monomers (64 core + 64 extended) have been hardened with a 0 panic guarantee: no monomer can panic, abort, or produce undefined behavior for any input in its declared domain. The security audit covers 14,500+ tests across 16 suites, including property tests, boundary tests, composition tests, and regression anchors. All arithmetic operations use wrapping semantics — not saturating — ensuring deterministic behavior at domain boundaries.

Closure Domains — How Circuits Close

For a circuit to be certified (Φ_c = 1), every monomer must declare its domain — the exact set of valid inputs and guaranteed outputs. No infinity. No undefined behavior. No surprises.

Domain Types

Type	Notation	Example	Cardinality
Range	`[min, max]`	u8 = `[0, 255]`	max - min + 1 = 256
Set	`{v₁, v₂, ...}`	bool = `{true, false}`	2
Bounded	`{x ∈ D \| P(x)}`	even ∩ `[0, 100]`	≤ \|D\|
Product	`D₁ × D₂`	ADD8 input = `[0,255] × [0,255]`	65,536

Why Domains Matter

ln(x)  where x ∈ (-∞, +∞)  → UNDEFINED (can produce -∞, NaN)  → Φ_c ≠ 1
ln(x)  where x ∈ [0.001, 1000000]  → BOUNDED output  → Φ_c = 1 ✓

The domain IS the circuit boundary. Without it, the circuit is open. The compiler enforces this: if any domain is unbounded, the program does not compile.

In Practice

Every core monomer (MC_00 to MC_63) has pre-defined domains:

ADD8: input [0,255] × [0,255], output [0,255] (wrapping)
HASH: input String(any), output String(hex, len=64)
IF: input {true, false} × Any × Any, output Any

When composing monomers through EVA algebra, the compiler automatically verifies that output domains match input domains of the next stage. If they don’t match, the circuit doesn’t close.

You Are the Circuit Designer

Like an electrical engineer who specifies voltage ranges for each component, you define the valid data ranges for your program:

// Airplane flight computer domains:
velocity:    [0, 900]    km/h  — commercial aircraft range
altitude:    [0, 15000]  m     — atmospheric flight ceiling
temperature: [-40, 1200] °C    — engine operating range

If a calculation produces velocity = 100,000, the circuit doesn’t close because the result violates the declared domain. The compiler rejects it. This is the fundamental difference:

Normal software: calculates 100,000 km/s, stores it, nobody notices until something breaks
Digital Circuitality: the program doesn’t compile — the circuit is open

Domains Are Numeric Ranges, Not Units

[0, 900] means “numbers between 0 and 900” — not km/h, not meters, not degrees. Units are the designer’s responsibility. The compiler only verifies numeric ranges.

Precision Is an Engineering Decision

Monomer Type	Range	Rounding	Certification
U8 (MC_00-07)	[0, 255]	None — wrapping mod 256	Φ_c = 1
I64	Full 64-bit	Truncation (7/2 = 3)	Φ_c = 1
F64 (MC_64-71)	IEEE 754	Floating-point rounding	Φ_c = CONTRACT

Need exact decimals? Use the fixed-point pattern: multiply by 1000, compute in integers, divide at the end. 3.14 becomes 3140. Zero rounding. Φ_c = 1. Need real decimals? Use F64 extended monomers. Accept CONTRACT certification. IEEE 754 rounding applies (0.1 + 0.2 ≈ 0.30000000000000004).

Certified Math at Any Precision

Any mathematical function — logarithms, trigonometry, square roots — can be implemented as a certified polymer (Φ_c = 1) using only core monomers with scaled integers. The designer declares the precision:

domain pi_3:  Range [3141, 3142];           // π with 3 decimals
domain pi_6:  Range [3141592, 3141593];     // π with 6 decimals
domain pi_15: Range [3141592653589793, ...]; // π with 15 decimals

Like choosing a 12-bit vs 16-bit ADC — the engineer decides the resolution. The “error” is not accidental IEEE 754 rounding. It’s the precision you declared in your domain. Result: ln(), sin(), cos(), sqrt() — all certifiable. All deterministic. Same input → same output on every platform, every time.

How Domains Are Designed Today

Built-in domains — Core monomers have pre-defined domains (ADD8 accepts [0,255]²)
Guard conditions — if (speed > 900) { return error; } creates a domain boundary
Monomer selection — choosing bounded operations (u8 arithmetic) vs unbounded
Policy circuits — PCD programs that validate inputs before processing
TCE verification — the compiler checks all paths produce values within domains

Domain Declaration (Planned Syntax)

PC flight_computer {
    domain speed: Range [0, 900];
    domain altitude: Range [0, 15000];

    fn calculate_eta(distance, speed) {
        // TCE verifies: speed ∈ [0, 900]
        // result automatically bounded
        return distance / speed;
    }
}

Quickstart

Get running in 5 minutes

PCD Language

Write your first circuit

Roadmap

Extended Monomers · Certification Registry · BPU Silicon

Getting Started

PCD Language

CLI Reference

Lifter

Transpiler

API Reference

MCP Integration

SDKs

Theory

Introduction

BRIK-64 — Digital Circuitality

128 Hardened Monomers

EVA Algebra

CMF Certification

Roadmap

Your compiled code ships with its test suite

Use BRIK-64 Now — In Any Language

Install

What Φ_c = 1 means in practice

Write PCD, compile to any target

The Core Monomer Catalog — MC_00–MC_63

Extended Monomers — MC_64–MC_127

Certification

The Coherence Foundation

Security Audit — v4.1.0-beta.1

Closure Domains — How Circuits Close

Domain Types

Why Domains Matter

In Practice

You Are the Circuit Designer

Domains Are Numeric Ranges, Not Units

Precision Is an Engineering Decision

Certified Math at Any Precision

How Domains Are Designed Today

Domain Declaration (Planned Syntax)

Quickstart

PCD Language

Roadmap

Getting Started

PCD Language

CLI Reference

Lifter

Transpiler

API Reference

MCP Integration

SDKs

Theory

​BRIK-64 — Digital Circuitality

128 Hardened Monomers

EVA Algebra

CMF Certification

Roadmap

​Your compiled code ships with its test suite

​Use BRIK-64 Now — In Any Language

​Install

​What Φ_c = 1 means in practice

​Write PCD, compile to any target

​The Core Monomer Catalog — MC_00–MC_63

​Extended Monomers — MC_64–MC_127

​Certification

​The Coherence Foundation

​Security Audit — v4.1.0-beta.1

​Closure Domains — How Circuits Close

​Domain Types

​Why Domains Matter

​In Practice

​You Are the Circuit Designer

​Domains Are Numeric Ranges, Not Units

​Precision Is an Engineering Decision

​Certified Math at Any Precision

​How Domains Are Designed Today

​Domain Declaration (Planned Syntax)

Quickstart

PCD Language

Roadmap

BRIK-64 — Digital Circuitality

Your compiled code ships with its test suite

Use BRIK-64 Now — In Any Language

Install

What Φ_c = 1 means in practice

Write PCD, compile to any target

The Core Monomer Catalog — MC_00–MC_63

Extended Monomers — MC_64–MC_127

Certification

The Coherence Foundation

Security Audit — v4.1.0-beta.1

Closure Domains — How Circuits Close

Domain Types

Why Domains Matter

In Practice

You Are the Circuit Designer

Domains Are Numeric Ranges, Not Units

Precision Is an Engineering Decision

Certified Math at Any Precision

How Domains Are Designed Today

Domain Declaration (Planned Syntax)