Engineering Blog
Technical writing, research, and proof-driven engineering.
Notes from the BRIK64 team regarding formal verification, systems architecture, and the future of certified software execution.
What Digital Circuitality Tries to Formalize
A bounded programming model built from reviewed operations, explicit composition, and closure checks. This essay explains the formal claim, its limits, and why it differs from testing.
Archive
Latest posts
Showing 31 posts total
Page 1 of 4
First PCD Circuit: A Minimal Walkthrough
Install the CLI, write a small circuit, and inspect the bounded output path. A practical introduction to the format and the compile step.
EVA Algebra: Sequence, Parallel, Conditional
How three composition operators carry sequencing, fan-out, and branching through the circuit model, and what that means for compiler readability and closure.
One Blueprint Across Multiple Targets
How the transpilation chain uses PCD as a bounded intermediate form, what 10 source languages and 14 targets mean in practice, and where the equivalence claim stops.
Why Tests Passing Is Not the Same as Closure
A look at sampled testing versus bounded verification, with examples of logic that passed tests but still required stronger structural checks.
COBOL Migration Through Bounded Lift-and-Review
Why legacy modernization benefits from lifting review-critical logic into a bounded blueprint before transpilation or replacement.
BPU: Policy Enforcement as a Hardware Roadmap
Why software-only guardrails share execution context with the model they constrain, and how the BPU roadmap moves policy enforcement toward FPGA and silicon.
Why AI-Generated Code Needs Blueprints and External Checks
Generated code and generated tests can fail together. This note explains why BRIK64 keeps verification outside the model loop.
PCD for AI Agents: A Small Format with an External Proof Loop
How a finite grammar helps agents author bounded logic while the compiler and policy checks stay outside the model.