# MOTO v1.0.8

## Features
  - Added LeanOJ Proof Solver as a third standalone mode with dedicated model profiles, cumulative brainstorming, proof storming, skip-brainstorm control, and Lean 4-verified final template solving.
  - Added hosted/generic-mode runtime support with an API-only sandbox contract, FastEmbed embeddings, OpenRouter-only inference, and capability flags for the hosted web wrapper.
  - Added pruned-paper preservation and history downloads so context-excluded Stage 2 papers remain reviewable by users.
  - Added "supercharge" mode that incorporates a mini-version of Top-P exploration at the individual model level. Increasing a model's intelligence before its final constituent answer within the harness itself. This has the largest impact on LM studio and budget model users that are running smaller models.
  - The brainstorm mechanic for all modes can now produce Lean 4 proofs in the brainstorm stage if relevant to the users prompt.

## Changes
  - Optimized proof-solving prompt flow to work directly toward the user prompt/template instead of only building exploratory context.
  - Added statement-alignment validation so Lean-accepted proof code must correspond to the intended theorem candidate before storage or placement.
  - Added shared proof registration and integrity gates across autonomous proof verification, compiler rigor mode, and LeanOJ.
  - Updated project rules to document hosted runtime behavior, LeanOJ, and shared proof-integrity architecture.
  - Added shared post-Lean proof integrity checks for autonomous paper proofs, compiler rigor mode, and LeanOJ.
  - Compatible models screen is now on all settings.
  - Added "Major mathematical discovery" validator ranking category for proofs and relabeled the gold category to "Minor Mathematical Discovery". Users are now able to tell which discoveries are major vs minor as per their validator model's direction injection review.
  - Optimized and audited .cursor rules folder to assist with vibe coders and forks.
  - Parallel ran harness roles now utilize a temperature ladder such as 0, .2, .4, and .8 for concurrent LM studio API calls on models loaded with multiple slots.
  - Expanded OpenRouter model/provider settings, raw settings tooling, and automated context settings to avoid provider outliers that disrupted automatic context sizing.
  - Improved API logging, boost routing visibility, and live activity UI for long-running workflow state.
  - Improved autonomous proof verification and paper context handling during brainstorm-to-paper and resume flows.
  - Improved compiler rigor, critique, and Wolfram tool flows.
  - Updated launchers, updater metadata, and Linux hosted entrypoint behavior.
  - Refreshed documentation, rules, ignore files, and test coverage.

## Bug Fixes
  - Hardened desktop API access with loopback defaults, token-authenticated HTTP routes, one-time WebSocket tickets, and CSRF-style origin checks.
  - Hardened hosted proxy auth with signed body-hash headers so unauthenticated request bodies are not buffered before rejection.
  - Hardened workflow startup, provider error handling, and log redaction paths for safer default and hosted operation.
  - Fixed Boost secret persistence so OpenRouter keys are no longer written to boost state and restored Boost reports when a key is needed.
  - Locked Z3 executable configuration to trusted startup settings and rejected runtime `z3_path` proof-settings input.
  - Hardened final-answer archive access against nested paper/brainstorm path traversal.
  - Hardened PDF export by sanitizing server-side HTML, enforcing size caps, disabling JavaScript, and blocking external Chromium requests.
  - Redacted API/Boost logs by default so full prompts, responses, Wolfram tool results, and legacy full payloads are not exposed through log routes.
  - Sanitized OpenRouter/provider error bodies before logging or surfacing them to avoid leaking echoed prompts or keys.
  - Removed OpenRouter API keys from model-list query strings and require headers or stored runtime keys instead.
  - Disabled hosted self-update mutation and made workflow start checks atomic across top-level modes.
  - Reduced proof-status path disclosure by returning safe Lean/Z3 path labels instead of absolute local paths.
  - Fixed retry transcript hygiene so private model thought/channel tokens cannot poison retries, memory, or RAG context.
  - Fixed Mathlib and Lean 4 co-dependence bug that disrupted some users' proof generation.
  - Rejected fake proof devices (`axiom`, `constant`, `opaque`) introduced by generated Lean code unless already present in the source/template context.
  - Fixed LeanOJ skip-brainstorm handling so the skip request is not consumed before the brainstorm phase.
  - Fixed generic API helper path handling so configured API bases are respected.
  - Fixed API call logs so standard model calls are recorded alongside boosted calls.
  - Fixed OS hover pop-up layering showing behind neighboring boxes.
  - Fixed OpenRouter credit exhaustion causing proofs to be skipped if the user ran out during the proof creation step.
  - Fixed RAG lock release on cancelled embedding/indexing tasks so resumed research cannot stall.
  - Fixed autonomous paper writer resume so completed brainstorms restart at the proof/paper handoff instead of zero.
  - Fixed manual Lean 4 proof checks so they use the currently selected role models instead of stale brainstorm or paper generation models.
  - Fixed Lean 4 proof completion UI so finished proof passes show accurate live activity counts.

  Authored by Patrick White, Patrick@Intrafere.com