v1.5.0

Fifth feature minor on the 1.x LTS line. Quint-inspired tooling additions:
literate workflow specs, ITF trace export, an interactive REPL,
random property-based workflow simulation with witnesses, and the
__builtin_debug print-and-passthrough helpers. The first bytecode
minor bump (1.0 → 1.1) under the additive-opcode contract.

Added

• Literate workflow specs (boruna literate extract) — borrowed from Quint's Literate Specifications. A markdown file with <lang> <filename> += code fences (where <lang> ∈ ax|boruna|quint) is the single source of truth for both the audit narrative AND the executable Boruna source. boruna literate extract <file.md> --out-dir <dir> walks the document, validates each fence, and emits per-file outputs that compile and run via the normal boruna run / workflow run paths. Idempotent: re-running produces byte-identical output. Path traversal and absolute paths are rejected at parse time with stable error_kind strings (literate.invalid_fence, literate.path_traversal, literate.absolute_path, literate.invalid_out_dir, literate.io). New module tooling/src/literate/, reusable from any caller including boruna-mcp. Example fixture at examples/literate/hello_literate.md. See docs/design-literate-workflows.md and docs/architecture-literate-workflows.md.
• ITF (Informal Trace Format) export from evidence bundles — borrowed from Quint / Apalache / the ITF Trace Viewer. boruna evidence inspect <bundle> --itf emits the bundle's audit log as an ITF v0.15 document on stdout, with one ITF state per audit-log entry and event variant names preserved as #meta.action. --itf is mutually exclusive with --json. Boruna's internal evidence-bundle format is unchanged — ITF is purely an export. Vendored producer constant ITF_FORMAT_VERSION = "0.15". New module tooling/src/trace/{itf,audit_to_itf}.rs. Spec source: https://apalache-mc.org/docs/adr/015adr-trace.html. See docs/design-itf-traces.md and docs/architecture-itf-traces.md.
• __builtin_debug(v) / __builtin_debug_msg(msg, v) — print-and-passthrough debug helpers (bytecode 1.1). Borrowed from Quint's q::debug. The single-arg form prints Value::Display form to stderr and returns the value unchanged; the two-arg form prints <msg> <value>\n. Operational-only — no capability gate, no audit-log event, no replay impact. Implemented as two new opcodes Op::Debug (0xA7) and Op::DebugMsg (0xA8); BYTECODE_VERSION bumped to "1.1". A 1.0 reader presented with either opcode MUST reject with an unknown-opcode error per §1.2(6) of docs/spec/bytecode-1.0.md. See docs/architecture-q-debug.md.
• boruna repl [file.ax] — interactive REPL for .ax modules. Borrowed from Quint's quint repl. Loads an optional initial .ax file, evaluates expressions, supports meta-commands :load, :reload, :reset, :type, :env, :help, :quit. Per-input compile + fresh VM (avoids module-frozen-by-construction VM invariants); the synthetic wrapper declares Int return type because the typechecker is currently permissive about return-type unification, and :type reports the post-hoc Value::type_name(). Defaults to --policy deny-all because REPL inputs are non-deterministic. No line-editing dep — uses std::io::BufRead, sufficient for piped agent-driven use. Bytecode 1.1's __builtin_debug works in the REPL. See docs/architecture-boruna-repl.md.
• boruna simulate <dir> [--invariant <expr>] [--witnesses name=expr,...] — random property-based workflow simulation. Borrowed from Quint's quint run. Runs the workflow --max-samples times (1..=100_000, default 1000) and reports invariant violations + per-witness trace frequencies. The invariant / witness DSL accepts status == "...", total_duration_ms < N, step.<id>.status == "...", step.<id>.duration_ms < N, combined via && / || with parentheses. Per project-conventions-2026-04 §15 the simulator's per-trace WorkflowRunResult is operational-only and never feeds production replay verification. Sequential v1; input fuzzing and parallel execution are documented follow-ups. Stable error_kind strings: simulate.invalid_samples, simulate.invalid_workflow, simulate.invariant_parse, simulate.witness_parse. New module orchestrator/src/simulate/{mod,invariant,witness}.rs. See docs/architecture-boruna-simulate.md and docs/architecture-boruna-witnesses.md.

Decided

• docs/spec/bytecode-1.0.md v1.1 minor bump — additive opcodes per §1.2(6) of the spec. Updates the version-identifier prose, adds §4.5 "1.1 additions" with the new opcode table entries (Debug 0xA7, DebugMsg 0xA8), and appends a §12 changelog entry. Backwards compatibility within 1.x is preserved: a 1.1 module CAN be rejected by a 1.0 reader (unknown-opcode error), but every 1.0 module continues to load on a 1.1 reader.
• Apalache-style bounded symbolic model checking is NOT recommended for Boruna. A pull-in of Apalache + Z3 + a Boruna IR → SMT translator would be a multi-engineer-year integration aimed at an audience (consensus-protocol provers) that does not appear in Boruna's compliance-runtime positioning. Boruna's concrete-trace + replay + evidence-bundle model is a different design philosophy and stays as-is. See claudedocs/research_quint_borrowable_ideas_2026-05-20.md.