Getting Started with Sekura JS

Guide version: 1.0
Implementation snapshot: SekuraJS source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236.

This guide starts from a licensed SekuraJS source checkout and uses the CMake build defined by the repository.

1. Install build and runtime dependencies

The build requires:

  • CMake 3.16 or newer;
  • a C++17 compiler;
  • ZLIB;
  • libsodium, required for Ed25519 SJP signatures;
  • Z3 available on PATH for SJV proof and SJP replay.

CVC5 is optional. It is used only when verify-sjp is run with --cross-check-cvc5. Install the dependencies using your platform’s package manager. On macOS, CMake checks the Homebrew prefixes /opt/homebrew and /usr/local for libsodium.

2. Build and install the command-line tools

From the root of the licensed SekuraJS checkout:

cmake -S . -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build --parallel
cmake --install build --prefix "$HOME/.local"

The build creates two CLI programs: sekura-js and sekura-sjv. The install step places them under $HOME/.local/bin. Add that directory to PATH if needed:

export PATH="$HOME/.local/bin:$PATH"

To use the build-tree binaries without installing them, run build/sekura-js and build/sekura-sjv from the repository root.

3. Check the installation

sekura-sjv --help
sekura-js check examples/verification_identity.sjs

The first command prints the SJV command summary and exits successfully. The second should print:

Syntax OK

sekura-js has no --version command. Its top-level help is printed when it is invoked without a command; the CLI reference documents the exact behavior.

4. Write and compile your first Sekura JS module

Create hello.sjs:

let r2: u32 = 0;

let identity(value: u32): u32 {
    return value;
}

Compile it:

sekura-js compile hello.sjs

With default options, compilation uses -O0 and writes these files beside hello.sjs for an ordinary runtime module:

hello.sasm
hello.sdef
hello.sobj
hello.smod

The compiler can update a named module declaration in the input source to persist a generated RegID. This sample has no explicit module declaration, so its module name is inferred from the source filename.

Compilation produces a Memora8/MR8 SOBJ. It does not run that SOBJ; the simulator is a separate project and is not built by this repository.

5. Check an SJV model

The repository includes this SJV example:

sekura-sjv parse examples/verification_identity.sjv
sekura-sjv verify-model examples/verification_identity.sjv

verify-model checks the SJV model and its consistency with the selected Sekura JS source. It does not verify a compiled SOBJ. For implementation verification, the command is:

sekura-sjv verify <model.sjv> <program.sobj> [environment.json]

The checked-in verification_identity SJS/SOBJ example currently reports FUNCTIONAL UNSUPPORTED for implementation verification. Its successful verify-model result must not be read as an implementation proof. See the SJV CLI reference for the separate command outcomes.

6. Run a positive first proof with the implemented SystemVerilog path

The current source tests include a small combinational adder whose SJV contract is proved by sekura-sjv. Create adder.sv:

module adder;
  function automatic logic [7:0] add(input logic [7:0] a, input logic [7:0] b);
    begin
      add = a + b;
    end
  endfunction
endmodule

Create adder.sjv beside it:

module "adder.sv";

{ 1 == 1; }

function add {
    return' == a + b;
}

Run the proof:

sekura-sjv verify adder.sjv

For this checked example, the verifier reports FUNCTIONAL PROVED and exits with status 0. The SystemVerilog path verifies the supported RTL subset directly; it does not compile SystemVerilog into SOBJ. Parsing or elaboration of other SystemVerilog syntax does not mean that syntax is supported by the proof backend. See the SystemVerilog subset reference.

7. Create, sign, and check an SJP

Generate an SJP for the same SystemVerilog proof:

sekura-sjv make-sjv adder.sjv adder.sjp

make-sjv writes an unsigned SJP v2 package. The command can return success after package generation even if the result recorded inside the package is not proved; inspect the reported result or verify the package after signing.

Create an Ed25519 keypair. Both output files must not already exist:

sekura-sjv keygen-ed25519 signing.secret signing.public

Sign the package to a different output path, then replay it:

sekura-sjv sign-sjp adder.sjp signing.secret adder.signed.sjp
sekura-sjv verify-sjp adder.signed.sjp --trusted-key signing.public

verify-sjp requires a signed SJP and an explicitly supplied public key. It validates the Ed25519 signature, checks the package, and replays the stored SMT queries with Z3. Successful replay prints SJP REPLAY MATCH and exits with status 0. The public key is caller-selected; the tool does not keep an organization trust store.

To request the optional cross-check, install CVC5 and run:

sekura-sjv verify-sjp adder.signed.sjp --trusted-key signing.public --cross-check-cvc5

This repeats the stored queries through CVC5 in addition to Z3. For details about key files, signature contents, replay checks, and result codes, see SJP Package Format and SJP Signatures.

8. What success means

  • sekura-js compile confirms that the compiler generated artifacts for the selected SJS input; it does not execute the resulting SOBJ.
  • sekura-sjv verify reports proof of the selected SJV contract only for the supported input path and modeled scope.
  • sekura-sjv make-sjv creates a package but does not sign it and does not make an unproved result into a proof.
  • sekura-sjv verify-sjp checks the signature and repeats the SMT queries stored in the SJP. It does not regenerate those queries from the original sources.

The CLI references provide the full compiler and verifier command syntax. The repository’s license describes use of the proprietary software.