Formal Methods

During October 19–25, Memora8 advanced its independent C++ emulator and the formal verification of its SystemVerilog RTL. mr8sim gained a more faithful eight-stage pipeline, per-page SRAM port arbitration, word-streamed PageMover and a persistent sparse 8 GiB SD image. Static and dynamic Sekura JS programs passed language tests; selected RTL/C++ traces matched 22/22 and 16/16 COMMIT events. The open Assurance Memora8 repository records 859 proved obligations, 51 expected counterexamples and 51 SJP packages for scoped properties across all 32 opcodes.

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.

Implemented SJP v2 container, manifest fields, integrity checks, Ed25519 attestation, and the exact scope of verify-sjp.

How sekura-sjv creates and checks SJP attestations, what the caller-supplied key establishes, and what it does not establish.

Implemented SystemVerilog subset, parser and proof boundaries, unsupported constructs, hierarchy, sequential logic, and examples.

SJV syntax, state blocks, function contracts, pre-state and post-state expressions, source binding, and current verification scope.

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.

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.

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.