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.

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.