Sekura JS

CLI reference for the Sekura JS compiler and assembler, plus legacy SJV command aliases accepted by sekura-js.

CLI reference for sekura-sjv at the current SekuraJS source revision, including inputs, defaults, outputs, and exit statuses.

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.

Versioned system requirements based on the current CMake configuration and CLI behavior.

Licenses and sources for external components used during Sekura JS builds, verification, and extension development.

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.

Syntax and implemented behavior for Sekura JS source files, including types, expressions, control flow, memory access, and modules.