From October 3 to 10, 2026, Memora8 added physical microSD, UART, and GPIO tests, integrated BLAKE3 and Ed25519 VERIFY, and optimized PageMover while retaining a routed 125 MHz eight-core Artix-7 build. This report summarizes the measured results and the next steps: a custom Ethernet controller and incremental formal verification.
Memora8 FPGA Implementation: 8-Core Artix-7 Status
As of October 4, 2026, the Memora8 FPGA implementation combines eight 32-bit CPU cores, 1 MiB of banked SRAM, MMU page windows, SYSTEM BUS devices, PageMover, DDR3/MIG connectivity, and UDP debug for the BX72 Artix-7 XC7A200T. The completed routed build meets 125 MHz timing, but the reported integration tests use a simulated DDR3/MIG and bypass physical Ethernet MAC/RGMII; board-level operation and the planned cryptographic accelerators remain future work.
Sekura JS Formal Verification: A First Step Toward Evidence for the Language
Assurance Sekura JS establishes an initial, inspectable evidence base for selected properties of compiled programs. This article explains the source-to-object-to-contract chain, the current evidence across five language areas, optimization profiles O0–O4, restricted preconditions, and why test results, formal proofs, signatures, and SMT replay must not be conflated.
Proof Without Disclosing Source Code: How SJV Contracts and SJP Packages Support Independent Verification
Source code may need to remain private, but verification evidence can still be shared. This article explains how SJV defines the properties under review and how an SJP package carries verification results and replayable SMT obligations. It distinguishes contract scope, package integrity, Ed25519 signatures, and proof provenance, and makes clear that replaying stored obligations alone does not prove they were generated from the claimed private source revision.
Sekura Noda Assurance: Requirements, Verification, and Engineering Evidence
Sekura Noda Assurance helps engineering teams preserve why a claim is supported for a specific system version. It links requirements, specifications, implementations, verification runs, and evidence; tracks coverage and freshness; and records immutable baselines. Noda organizes evidence but does not run verification tools or certify compliance with industry standards.
Formal Verification of SystemVerilog in Memora8: RTL Contracts and Proof Scope
Memora8 is developing a formal verification path for real SystemVerilog modules. This article explains why simulation and formal methods complement each other, how RTL properties are checked, what the current SystemVerilog subset supports, how SJP binds results to RTL and contracts, and why verification claims are made property by property.
Memora8 Memory Architecture: K4,4 Topology Closes 125 MHz Timing on Artix-7
A report on finalizing the baseline Memora8 cluster memory geometry: 8 CPUs, 16 physical shared banks, 32 logical banks, 128 pages of 8 KiB, and 1 MiB SRAM. The K4,4 topology routed on an Artix-7 XC7A200T at 125 MHz with positive timing slack and one-cycle CPU reads; full integration with the MMU and other processor blocks remains to be verified.
Sekura JS Formal Verification: Proving Compiled Programs Against SJV Contracts
Sekura JS now verifies the compiled SOBJ artifact against formal SJV contracts. This article explains the source-to-proof pipeline, preconditions, postconditions, symbolic execution, SAT and UNSAT results, counterexample diagnostics, verification identity, and the limits of the current system.
Memora8 on Artix-7: From Simulator to a Working FPGA Processor
Memora8 has moved from the mr8sim simulator to a working networked MR8 processor on an Artix-7 XC7A200T FPGA. This report explains the hardware profile, transport protocols, memory ownership model, timing work, verification results, and next steps.
Sekura Talk Begins Public Testing | A Live Conversation Without History
A first post in the Sekura Talk cycle: why we built a live conversation layer without permanent history, how it works, and what public testing is meant to validate.