Sekura JS is a proprietary compiler and verification toolchain for Memora8/MR8. This section documents the sekura-js compiler, the sekura-sjv verifier, the sekura-sjs VS Code extension, and the source and artifact formats they support. These guides describe implemented behavior and identify known limitations.
Language and verification
- Sekura JS Language Reference — source files, types, expressions, statements, functions, modules, and documented language behavior.
- SJV Verification Language Reference — state models, function contracts, preconditions, post-state relations, and implementation verification.
- SJV-SV SystemVerilog Subset Specification — supported SystemVerilog profile, RTL semantics, proof scope, and verified implementation coverage.
- SJP Format Specification — replayable proof packages, exact SMT obligations, integrity, Ed25519 attestations, and dependencies.
Tools and workflows
sekura-jsCommand-Line Reference — compilation, assembly, optimization profiles, module outputs, and artifacts.sekura-sjvCommand-Line Reference — SJV/SJP generation,verify-sjp, SystemVerilog verification, signing keys, solver options, and exit codes.- Getting Started — building the tools, compiling a first program, verifying a contract, and replaying an SJP.
- Generated Artifacts — purpose and relationships of
.sobj,.smod,.sdef,.sasm, and other generated files. - Examples — examples for compiling Sekura JS, checking SJV, proving supported SystemVerilog, and creating and verifying signed SJP packages.
- Diagnostics and Exit Codes — CLI output and process exit behavior for shell scripts and CI.
Reference
- SJP Signatures and Verification — Ed25519 signing, public keys, signature validity, and the distinction between signature verification and key trust.
- Compatibility and Versioning — product and artifact version markers, compatibility behavior, and documentation policy.
- System Requirements — initial distribution targets, source-build prerequisites, and runtime dependencies.
- Known Limitations — confirmed limitations of the language, compiler, verifier, SystemVerilog subset, and artifact formats.
- Releases and Changelog — current unreleased source snapshot and the format for future release notes.
- Licensing — binary use and redistribution, third-party components, user-created SJP artifacts, and the full license.
- Third-Party Notices — external libraries, solvers, extension test dependencies, licenses, and implementation provenance.
Each reference page identifies the implementation snapshot it describes. Consult the Known Limitations page for boundaries that apply across the toolchain.