Releases and Changelog

Page version: 1.0
Current source snapshot: 6dd5716a8f3bcf29d27ae9ca64800bb517601236 (2026-09-26).

This page records product release notes and compatibility changes. The source repository at the snapshot above has no product release tags, and the sekura-js and sekura-sjv CLIs do not expose release version numbers. The section below describes the current development snapshot; it is not a published or supported product release.

Unreleased — current development snapshot

Added

  • sekura-js, the Sekura JS compiler targeting Memora8/MR8, with the existing compile and assemble command families.
  • sekura-sjv, a separate CLI for SJV model operations, implementation/RTL verification, SJP generation, signing, and replay.
  • A direct verification path for the implemented SystemVerilog subset. SystemVerilog is not compiled into SOBJ.
  • SJP v2 ZIP generation and signed-package replay. Ed25519 signing uses libsodium; replay uses Z3, with an optional CVC5 cross-check.
  • The sekura-sjs VS Code extension remains a separate component in the repository.

Compatibility

  • The MR8 SOBJ reader accepts format version 0x00010000.
  • Current SJP generation writes format version 2. The legacy line-oriented SJP v1 representation is not replayable by the current verifier.
  • SJP proof-semantics identifiers distinguish the MR8 SJS/SOBJ path from the SystemVerilog path; they are not product release numbers.
  • Initial distribution targets are Windows x64 and macOS Apple Silicon. Other platforms are handled on request; this source snapshot does not constitute a packaged release for either target.

Known limits

  • The supported SystemVerilog constructs and proof boundaries are documented in the SystemVerilog subset reference.
  • The SJS/SOBJ proof backend supports a narrower expression set than the parser; see SJV Language Reference and Known Limitations.
  • make-sjv may write a package containing an unsuccessful or inconclusive proof result. Package creation does not imply proof success.

Release-note structure

For each actual shipped release, add a dated section in this form. Do not assign a version until product artifacts are built and the version is recorded in the release process.

## [X.Y.Z] — YYYY-MM-DD

Source revision: `<full Git SHA>`
Platforms: Windows x64; macOS Apple Silicon (arm64)

### Added
- User-visible language, compiler, CLI, or verifier capability.

### Changed
- Changed behavior, defaults, diagnostics, or proof semantics.

### Fixed
- User-visible defects corrected in this release.

### Compatibility and migration
- SJS/SJV source compatibility changes.
- SOBJ or SJP format/semantics changes and required migration or replay behavior.
- Compatibility with prior tool and artifact versions.

### Security
- Signing, key handling, or security-relevant changes.

### Known limitations
- Important remaining limitations for this release.

Use only applicable sections; omit empty ones. Release entries should describe observable changes and call out incompatible behavior explicitly. Keep compiler/language changes, CLI changes, SJV proof behavior, SJP format/signature changes, and compatibility notes distinguishable. Record the exact source revision and platforms actually packaged and checked; list other supported platforms only when validated or explicitly available on request.

Versioning references

Product versions, SOBJ/SJP format versions, attestation versions, and proof-semantics identifiers are separate. See Compatibility and Versioning for the current markers and compatibility policy. See System Requirements for the initial platform targets and build/runtime dependencies.