Evidence before conclusion

The mental model

The name is a description, and the honest way to read this page is to take it apart. Symbolic because the system decides by evaluating declared symbols and rules rather than raw impression — which is a property of the whole pipeline, not only of the reasoning inside a phase. Evidence-gated because deterministic checks run before a candidate answer can be published. Orchestrator because the model never picks the route.

Start with how far the first word reaches, because it is easy to file “symbolic” under REASON and move on. The route itself is derived by a Prolog program from extracted facts, and the program reports the rule that produced the plan and whether that plan was unique. The evidence obligations, and the authority that owns each one, are Prolog facts. Tool permissions are a declarative boundary the chosen route cannot override. Evidence is bound to its source by content hash, and two renderings of a sentence are compared through a canonical identity rather than a fuzzy match. Completion is decided by checking declared state against each authority’s obligations — among them whether every decidable claim’s class has been discharged by the one procedure fixed to it.

So the symbolic layer is not a reasoning style available to one authority. It is the decision layer of the entire orchestration: routing, obligation, permission, binding, and verdict are all formal evaluation over declared symbols. The model contributes interpretation at exactly two points — extracting the triage facts, and reasoning inside a phase — and neither of those points is where a verdict comes from.

The authorities are where the idea becomes visible, and each realizes it differently. REASON derives its conclusions by executing a Prolog knowledge base. CODE registers decidable claims in a runtime-owned, revision-bound CODE Formal Model, where a claim’s class fixes exactly one procedure that must discharge it — a knowledge-base query, an approved typecheck, an SMT formalization, or the maths bridge. MATHS works in SymPy, Z3, and Lean. Three mechanisms, one posture: nothing counts because it was asserted.

The load-bearing sentence is this one: a temperature-zero model extracts what evidence a request requires, runtime-owned SWI-Prolog derives the shortest valid authority sequence from those facts, each authority executes its own native workflow, and a final-candidate verifier refuses to publish until the gates pass.

What makes it more than a prompt wrapper is where authority sits. The model classifies and reasons; it does not certify. Tool output cannot declare its own workflow completion, and the runtime-owned Prolog harness cannot be redefined by model code. Every terminal answer carries a status the model did not get to award itself.

Where SYMEVO fits

SYMEVO is a verification orchestrator, and the orchestration is the unit of capability — not the individual model call. A single request can be routed across authorities, and obligations cross between them.

Two examples, both from the policy layer. A CODE claim of class constraint is discharged by SMT — the same entailment authority REASON uses, which is why the SMT controller has to stay reachable from CODE. And the CODE↔MATHS bridge runs create_manifest in CODE, proves the exact claim with maths_problem, then accepts the runtime-recorded certificate back in CODE. Neither capability belongs to any single authority. Both are properties of the composition, and neither is reducible to one of its parts.

That is the part worth being precise about. A model call produces text; the orchestration produces a decided answer, and it can do so because routing, obligation, permission, binding, and verdict are all formal — which is what lets independently verified results be composed into something no single authority, and no single call, could establish on its own. What the system can reach is a function of how its parts are joined, not of the model alone.

The three authorities are the clearest statement of what it is for, and they come with a filter.

The filter

• The answer has a checkable form. A computation you can run, a change you can diff and test, or an argument you can derive from explicit premises. If “correct” has no mechanical witness, there is nothing here for a gate to consume.
• You would rather be told INCOMPLETE than be told something fluent. The system is built to refuse. If a confident paragraph is what you actually need, this is a great deal of machinery for a worse experience.
• You can state the premises. For REASON, the derivation is only as good as what you hand it — and SYMEVO verifies internal consistency, not premise truth. You remain the source of the premises.

What the three authorities replace

The wrong tool

• Open-ended writing. There is no gate for prose quality, and no authority owns it.
• Facts you need to be true. SYMEVO can ground a claim in a source you opened, but it does not verify that the source is right. Search results are discovery only.
• Latency-critical paths. A turn runs a classifier, a Prolog process, an authority workflow, and a verifier. There is a per-turn deadline (default 30 minutes) and it is not a small number.
• Anything where you want the model's own judgement trusted. That is the thing the architecture is built not to do.

Setup and the authorities

The package is @evo-ai/agent v2.0.0, ESM, Node ≥ 22.19. Model calls go to DeepSeek by default, or Together AI, and everything else is optional until a request needs it.

npm install
cp .env.example .env        # then set DEEPSEEK_API_KEY
npm run build               # clean + tsc + make-cli-executable + copy-assets
npm start                   # node dist/cli.js

npm link                    # optional: exposes the global `evo-ai` bin
npm run serve               # node dist/server/entry.js — the public web server

Only the tools a particular request invokes need their dependencies. CODE work does not require SWI-Prolog, Python, or Lean; a pure REASON turn does not need Chromium.

Python packages for the workspace virtualenv live in requirements.txt: sympy, numpy, scipy, scikit-learn, z3-solver, matplotlib, plotly, networkx, mplfinance, pandas, yfinance, kagglehub, datasets. Z3 is pinned to 4.15.4.0 deliberately — the comment in the file notes that 5.0 currently lacks a Linux ARM64 wheel.

Running the CLI

The CLI is flags-only. There are no subcommands — no serve, chat, or install verb. npm run serve is an npm script that runs a different entry point, and browser chat is a --chat flag.

evo-ai "prove that the sum of two even integers is even"
evo-ai --workspace /path/to/repo "add a retry to the upload client"
evo-ai --chat                    # serve the browser chat and open it
evo-ai --chat-port 8080          # implicitly enables --chat
node dist/cli.js "..."         # the same thing without npm link

The flags

There is no --version flag and no -- argument terminator; any unrecognized -x throws Unknown option.

Two run modes

If both stdin and stdout are TTYs you get the interactive terminal UI. Otherwise SYMEVO runs one-shot: it reads the prompt from the arguments or from stdin, prints the answer, and exits. That fallback is what makes it usable in a pipe.

Slash commands

Keyboard: Escape cancels a running turn. Ctrl+C interrupts a running turn, otherwise clears a non-empty editor, otherwise exits. Shift+Enter, Ctrl+Enter, and Alt+Enter insert a newline.

The evidence gates

Every authority has a native notion of evidence, and the gate is the set of obligations that must be satisfied before a candidate answer is published. The gates are deterministic checks, not another model opinion.

What counts, per authority

Only MATHS calls its levels rigor. CODE has a level too — CodeVerificationLevel, set with verification_level=mathematical or verification_level=implementation_bound_formal in the request — and it gates just as hard: any level above standard demands a source-bound verification manifest whose declared level must match, and implementation_bound_formal additionally demands a refinement proof the runtime cannot yet produce.

REASON declares no level at all, and that is the interesting part. Its obligations are not selected by a dial the caller turns; they are derived from the evidence kinds the request requires. Ask for something needing constraint entailment and SMT becomes an obligation; ask for a conceptual proof and Lean does. The rigor is an output of triage, not an input to it.

The REASON rule is stated flatly in the system prompt: the Prolog derivation is the evidence. Not a description of one, not a summary of one.

What never counts

• Model prose. Never evidence by itself. Model knowledge is not a tool result and must not be described as verified or externally sourced.
• The inbuilt knowledge base. evo-kb.pl describes the runtime’s own tool and configuration surface. Its own header says it is “self-knowledge only … a premise source, not evidence; no verification gate consumes it.” The query_kb tool repeats the warning in its description.
• Search output. Discovery only. Snippets must be registered as claims with ground_claims before anything may reason over them, and absence from a search is not proof of non-existence.
• A matrix of green tool calls. Command success does not establish semantic relevance, and it is not proof that a test suite is exhaustive.
• A consistent knowledge base. Consistency shows the submitted model derives its conclusion consistently. It does not show the premises are true.

How a candidate is gated

Two tiers. First, the workflow controller reports the first unmet obligation for the active authority — a missing problem_spec/1 artifact, a declared requirement that was never validated, an SMT obligation with no definitive verdict, a Lean obligation with no machine-checked proof, a diff that was never inspected. A candidate must also reproduce runtime strings verbatim: the REASON answer gate requires the seven canonical headings and exact copies of the runtime’s conclusions, assumptions, [DEPENDS] pairs, and requirement verdicts.

Second, the final candidate is evaluated once more — conflicting status declarations, dissolution approval, correctness certificates, and a regex that rejects forbidden Lean tokens: sorry, admit, axiom, unsafe, native_decide, exact?.

A rejection is not fatal. Feedback returns to the same loop. But rejections are bounded — after EVO_MAX_VERIFICATION_REJECTIONS (default 4) the turn returns INCOMPLETE.

The four terminal statuses

# every terminal answer carries the status the model did not award itself
[STATUS: SOLVED - authority: REASON]
[STATUS: INCOMPLETE - authority: MATHS]

# REASON status assignment, from the workflow prompt
#   all requirements fulfilled      -> SOLVED
#   partial                         -> MAPPED
#   none or failed                  -> INCOMPLETE
#   premises unsound                -> DISSOLVED

Semantic triage

Triage is called the Evidence Router, and its design rule is the most interesting thing in the system: the model extracts meaning, the runtime chooses the route.

A temperature-zero model run returns strict JSON and nothing else. It is a fact extractor, not a router. It reports the action, the target, the criteria the request implies, any operations requested, an explicit tier if you named one, and the proof mode. Then it stops. On the typed schema_version 2 path, model-supplied phases and evidence_requirements are ignored — the route is not the model’s to pick. A legacy compatibility path is still accepted for stored or older classifier responses, and that path does read them.

// what the model may say (schema_version 2)
{
  "action":  "prove",      // prove | review | diagnose | explain | how_to |
                          // implement | refactor | test | git | general
  "target":  { "id": ..., "description": ..., "source": ..., "support": ... },
  "criteria": ["mathematical_proof"],   // from a fixed vocabulary of 14
  "operations": [],                    // user-only attribution; never the model's request
  "proof_mode": "first_principles",
  "unresolved": [], "alternatives": []
}

// what the model may NOT say
//   "phases": [...]        -- ignored on the schema_version 2 path.
//   "tier": "MATHS"        -- only honored when the user named it explicitly.

Targets are open-ended entity descriptions, not members of a fixed taxonomy — that was a deliberate change, so the extractor is not forced to bend a novel request into a known category. Provenance is checked: for facts attributed to the user, the context, or an observation, the quoted support must literally occur in that input.

That check buys traceability, and the documentation is careful about what it does not buy: a matching quotation does not prove that the model interpreted it correctly.

What Prolog does with the facts

% criteria map to the evidence kinds that satisfy them
criterion_evidence(argument_quality, conceptual_derivation).
criterion_evidence(source_inspection, workspace_source).
criterion_evidence(runtime_results, runtime_behavior).
criterion_evidence(mathematical_proof, mathematical_proof).
criterion_evidence(constraint_entailment, smt_entailment).
criterion_evidence(conceptual_proof, lean_proof).

% obligations, then owners, then a shortest valid sequence
required(E) :- criterion(C), criterion_evidence(C,E).
required(assumption_analysis) :- criterion(assumptions).
required(workspace_source) :- operation(workspace_mutation).
required(repository_state) :- operation(O), memberchk(O,[commit,amend,push,create_pr]).
required_owner(O) :- required(E), owner(E,O).
allowed(O) :- required_owner(O).
allowed(O) :- explicit(O).

% the default is REASON only when nothing else is required or named
allowed(reason) :- \+ required(_), \+ explicit(_).

% a CODE -> MATHS -> CODE bridge must be a subsequence, not a jumble
bridge :- bridge_requested, allowed(code), allowed(maths).

Selection is shortest-phase-count, and the program enumerates candidate plans before cutting, so a cut can never hide a competing shorter plan. The search is bounded to 7 phases. Ties break stably by Prolog term sorting and are recorded as non-unique rather than silently resolved.

Planning optimizes nothing else. Not latency, not token cost, not model confidence, not expected success.

Routing statuses

A plan can be resolved and still carry unique: false. Uniqueness and resolution are independent.

The certificate

Every triage emits a certificate carrying the routing status, the extracted semantics, the plan, the evidence requirements and coverage, assumptions, the proof trace, and a SHA-256 of its own contents. Its engine is lite_reason_prolog, or degraded_deterministic if extraction or the Prolog call failed — in which case routing falls back to needs_observation and missing intent is not reconstructed from keywords.

When routing is unresolved, or when the model emits [REASSESS TRIAGE] on its own, the plan can be reassessed — at most three times per turn. Reassessment requires new successful observations after the first attempt, retains completed phases and the certificate hash, and freezes mutation and publish permissions. It cannot escape into an authority that was never planned.

Reasoning strategies

Behind a flag that defaults to off sits a portfolio of reasoning operators, each implemented as a Prolog search over an explicit finite model. It is the most experimental part of the system, and the code says so.

# the only two accepted values; anything else throws at startup
EVO_REASON_STRATEGY_MODE=on
EVO_REASON_STRATEGY_MODE=off    # default

With the portfolio off, the reason_strategy tool is not even registered, and the controller fails with Strategy portfolio is off (EVO_REASON_STRATEGY_MODE=off). The tool takes describe, status, and solve.

The operators

Operators are organized into five layers — reformulate, derive, explore, complexity, verify — and the available set includes deduction, forward chaining, working backwards, constraint satisfaction, counterexample search, optimization, generate-and-test, reduction, abstraction, analogy, recursive decomposition, divide-and-conquer, dynamic programming, search, means-ends analysis, greedy, randomized exploration, hypothesis-test-revise, and abduction.

Seven operators are registered but explicitly unavailable, and the distinction is enforced in the registry rather than left to documentation: induction, causal_reasoning, simulation, adversarial_reasoning, invariant_discovery, relaxation, approximation.

Selection is deterministic

strategy=auto uses that table; naming an operator directly requires it to be eligible. Repeating an unchanged attempt is blocked — “Repeated unchanged strategy attempt blocked; inspect its result or materially revise the problem.” Budgets are shared and reserved up front: 20,000 work units, 24 attempts, depth 20, 10 seconds.

Outcomes that refuse to overclaim

An attempt reports one of proved, refuted, feasible, optimal, plausible_hypothesis, infeasible, or unknown, and always carries the scope submitted_finite_model. Results are validated outside the solver — witnesses are rechecked against the original domains, proved requires exhaustive search, and a decomposition only counts as proved if every child was accepted. An unknown outcome becomes inconclusive with the reason kept intact: “No conclusion followed within the submitted finite model; uncertainty retained.”

The harness narrates its own limits in the code, which is unusual and worth quoting:

• “Positive Horn closure; failure to derive does not prove negation.”
• “No feasible assignment found. Inconsistent premises do not prove a claim.”
• “Missing predictions are not confirmation. Suggested tests have not been performed.”
• “a greedy dead end is not proof of impossibility”

Prolog and the derivation engines

SWI-Prolog is not a library call here — it is the derivation authority for symbolic, assumption-laden reasoning, and the runtime owns the harness so the model cannot replace it.

Four .pl assets ship with the runtime, and all four are runtime-owned. The first two carry an explicit “do not edit or redefine” stamp; the generated knowledge base says only “do not edit”:

For prolog_exec the model writes only a declarative knowledge base; the harness supplies everything else, and each call is isolated. Resource limits are deliberate: a 256 MB Prolog stack, a 25-second Prolog execution limit, and a 30-second outer process timeout with cancellation support.

The REASON workflow runs R1 SETUP through R6 ANSWER, and the step whose failure is most instructive is R4, the assumption-dependence test: the harness retracts and reasserts each assumption to see which conclusions actually depend on it. The system prompt warns that an assumption declared as a static rule rather than a dynamic fact survives retraction and makes the test useless — a silent way to pass a check that did nothing.

The other engines a REASON derivation can use

Prolog is the spine of REASON, not the whole of it. Some obligations cannot be discharged by a hand-written knowledge base — a decidable entailment over arithmetic, or a formal proof of a conceptual claim — and for those the authority reaches for a different engine. Triage chooses which, by mapping the requested criterion to an evidence kind REASON owns: constraint_entailment to smt_entailment, and conceptual_proof to lean_proof.

What keeps this orchestration rather than a tool grab-bag is the binding rule. An auxiliary engine does not get to assert its own conclusion: it must name the spec_requirement/2 it discharges, through requirement_id, and the runtime rejects a verdict whose id does not appear among the knowledge base’s declared requirements. The engines discharge named obligations inside the derivation rather than replacing it — the gate’s own comment is exact about this: SMT entailment “certifies a claim within the KB — it does not replace the derivation.”

Note also what REASON may not reach for. Raw z3_smt is denied in this tier, and the policy says why: REASON uses smt_entail for decidable entailment claims, and must declare its facts, policy, claim, and requirement id rather than hand a solver a free-form query. The ungated solver is withheld; only the mediated one is exposed.

The knowledge base is not evidence

This is the distinction most likely to be misread, so the codebase states it in three places. evo-kb.pl is self-knowledge: it describes the runtime’s own tools and configuration. Its header says it is “a premise source, not evidence; no verification gate consumes it.” The query_kb tool description repeats that the self-knowledge “is not verification evidence.” And the knowledge base’s own status predicate reports its size — at generation time, 74 tools and 75 configuration keys.

Two other query surfaces exist and are easy to confuse with it. query_kb exposes session predicates such as recent_messages/2, messages_about/2, tools_used_list/1, and search_conversation/2. query_proof_kb exposes the proof ledger: verified_lemmas/1, proof_errors/1, goal_snapshots/1, tactics_for_goal/2, errors_for_goal/2, similar_to/2.

Independent review and dissolution

DISSOLVED is the one status a model cannot award itself. Claiming a request is unanswerable is the most consequential thing an agent can say, so it costs an extra review with its own evidence requirements.

The rule: a status label, a consistent Prolog knowledge base, or a model-authored list of fulfilled requirements cannot establish that the user’s request is unanswerable. When a candidate declares DISSOLVED, the runtime makes a separate temperature-zero model call with no tools, handing it the original request, the candidate, the reference context, and the current phase’s tool records.

Approval is not a vibe. Every one of these is validated in code before the status is accepted:

• approved === true, and request_preserved — the reviewer is judging the request that was actually asked
• whole_request_blocked and blocking_demonstrated — the whole request, not a convenient part of it
• reasonable_repair_available === false — no reasonable interpretation salvages it
• an empty unsupported_assumptions list
• a nonempty premise_quote that literally occurs in the original request
• at least one interpretation, every one of them marked answerable === false
• exact quotes of tool output — failed, truncated, or non-matching citations invalidate the approval

The approval is bound by SHA-256 to the request, the candidate, and the full current-phase tool snapshot. A later candidate cannot reuse an earlier approval. A bare DISSOLVED with no approval is rejected with a message that says exactly why:

[SYSTEM] DISSOLVED requires independent review of the original request,
blocking evidence, and reasonable interpretations. A status label or
successful derivation alone cannot authorize dissolution.

The reviewer sees the latest 12 tool records from the current phase, each truncated to 12,000 characters. The request and the candidate are never truncated. A truncated record cannot serve as an accepted citation, which closes the obvious trick of citing something the reviewer could not read.

The tool surface

74 tools, generated from the live registry rather than written by hand, so the documentation and the code cannot drift.

The stated design intent is that the tools carry their own discipline in their descriptions. A few worth reading closely:

• git is strictly read-only inspection with operation-specific fields. Arbitrary Git arguments are not accepted, so there is no argument through which to smuggle a write.
• code_sandbox_run runs in an ephemeral OS sandbox with network disabled by default; enabling it requires an explicit user request.
• smt_entail is a deterministic verifier over a restricted grammar (QF_LIA, QF_LRA, QF_LIRA, QF_Bool) with four verdicts: PROVED, REFUTED, UNDERDETERMINED, INCONSISTENT.
• x_twitter exposes 70+ operations, and every write requires confirm=true plus user credentials.

The CODE workspace

CODE is the authority where evidence is easiest to fake and easiest to check, so the workflow is built around one question: what did you actually observe, and what did you actually run?

The workflow is K1 INSPECT through K5 ANSWER, and the gate consumes three things: that the sources were inspected, that the post-mutation diff was inspected, and that a native build or test actually ran. A directory listing, a web result, a scratch pad, a subagent’s answer, or a Prolog fact are all explicitly not exact-source evidence for CODE.

read / ls / grep / symbols     # inspect — the evidence base
edit                            # atomic, revision-checked; replace_text never truncates
undo                            # revert
bash                            # verification commands set codeVerified=true
code_symbolic_claim             # register a decidable claim for formal discharge
verify_plan                     # plan checks must be verified
code_sandbox_run                # ephemeral OS sandbox, network off by default
publish                         # gated on the above

edit is revision-checked and atomic, and its replace_text mode is documented as the preferred way to edit precisely because it never truncates the file. Destructive bash commands are refused. Verification commands — test, check, build, lint — are the ones that set codeVerified.

The CODE Formal Model

CODE has its own symbolic layer, and it is easy to miss because it looks nothing like Prolog. code_symbolic_claim registers a decidable claim and binds it to the exact source it came from. The claim’s class then fixes exactly one procedure that must discharge it, and no weaker substitute is accepted.

Registration asserts nothing by itself. Every formal fact must be bound to a source excerpt that actually occurs inside the cited line range, so a model-supplied “fact” is a candidate and never authority, and a source/excerpt mismatch is rejected outright. Constraint claims additionally require a non-vacuous support set.

Claims are bound to a workspace revision, and any revision change invalidates the discharge. That is what keeps a verified claim from outliving the code it was verified against — edit the file and the claim goes back to being unproven, rather than quietly remaining true about a version that no longer exists. A mutation marks the claim stale, clears its verdict and bindings, and names the changed paths that intersect its support.

The gate is additive: a read-only CODE turn that asserts no decidable claim carries an empty claim set, so this never fires, and ordinary CODE work is unaffected. Note also where constraint claims go to be discharged — to SMT, the same entailment authority REASON uses. A CODE turn can reach into another authority’s symbolic machinery, which is exactly why “symbolic” cannot be filed under one tier.

Where CODE evidence stops

The CODE authority documentation is candid about the edges of its own guarantee, and two of them matter if you are going to rely on this:

• No guarantee against concurrent writes after the last observation, and no proof that a test suite is exhaustive. The diff you inspected is the diff that existed when it was inspected.
• A Lean proof about a model of your source is not a proof of your source. That evidence is tagged assurance: source_linked_model_proof with implementationBound: false, and an implementation-bound formal request cannot complete or publish on it. Closing that gap needs a trusted source-to-model refinement checker — not another model assertion.

Source-anchored review notes remain an optional review ledger, explicitly not a completeness certificate.

Formal and mathematical work

MATHS is the deepest authority, and the one where the system is most insistent that a proof about the wrong statement is worse than no proof at all.

The workflow runs M0 START, M1 MODEL, M2 EXPLORE, M3 DERIVE, M4 VERIFY, M5 ANSWER. Rigor determines what closes it, and formal rigor is two-phase: the proof phase runs M1–M4 to produce a frozen mathematical certificate, and only then does the Lean extension phase begin — prove_problem start, a statement skeleton, then either a direct track or a decomposition track, ending in verify_final.

The gate rejects the standard ways of faking a Lean proof. A regex refuses sorry, admit, axiom, unsafe, native_decide, and exact?. Evidence is bound to exact source hashes. A failed proof route is deferred and replanned — never silently treated as proved.

If the formal phase times out, the frozen mathematical certificate is still rendered as the answer, and only the Lean formalization is marked incomplete. That is a deliberate separation: the maths was done, the mechanization was not.

Formal recovery

When a Lean proof stalls, recovery is guided rather than blind. The controller renders its allowed next actions as workflow guidance, and a frontier_plan accepts Lean identifiers only — pending lemmas must be registered with an exact statement and dependencies before they can be probed or delegated, and registration rejects unknown dependencies and cycles.

Failed executions and probes increment the registered frontier’s attempt count; missing arguments and protocol errors do not. At EVO_AUTO_SPLIT_THRESHOLD (default 3) the controller suggests specialist workers, then explicit decomposition.

Configuration

Around 75 environment variables, all documented in .env.example and in the generated configuration reference. Precedence is constructor overrides, then process environment, then a .env in the source directory.

Parsing behavior worth knowing

• Integers ignore zero and negatives. The parser requires a value greater than zero and otherwise falls back to the default — so EVO_MAX_TURN_MS=0 does not mean “unlimited”, it silently means 1,800,000.
• Booleans are permissive. Anything not in disabled, off, false, 0, or no reads as true. Setting a variable to a value you did not intend can enable a feature rather than disable it.
• EVO_REASON_STRATEGY_MODE is strict, and throws on anything that is not exactly on or off — the opposite of the boolean rule above.

One documented default deserves a callout rather than a footnote: the Gmail integration ships a non-placeholder default account address in .env.example and in the generated configuration reference. Set GMAIL_ACCOUNT explicitly rather than relying on the default.

Gotchas

• --no-stream does nothingThe flag is parsed into a field that is never read again. The --help text (“Disable streamed one-shot output”) is misleading; the README correctly calls it an accepted compatibility flag.
• --extra-workspace is hiddenA real, repeatable flag that appears in neither --help nor the README. Only its environment equivalent, EVO_EXTRA_WORKSPACES, is documented.
• --chat-port turns chat onPassing a port implicitly enables --chat and opens a browser to a token-bearing localhost URL.
• The log path documented in the README is wrongThe README says logs default under .evo/logs/. The code defaults to <EVO_ARTIFACT_ROOT>/logs/evo.log. EVO_LOG_PATH overrides both.
• No --version, no --There is no version flag and no argument terminator. Any unrecognized -x throws.
• EVO_REQUIRE_LEAN does not fail bootIts name and its description in .env.example both say it should stop the server when the Lean smoke proof cannot run. The code does not: enabling it runs a startup preflight, and a failed preflight only logs a warning and continues, so the platform healthcheck still passes with the Lean-dependent tools disabled. Nothing fails fast.
• Missing JWT_SECRET is a hard boot failureThe server refuses to start, and the error message explains the alternative: every session token would be forgeable.
• code_worker is a stubIt is registered as an unavailable compatibility adapter and tells you to use evo_subagent instead.
• Documented tools may be unavailableThe docs generator hard-codes the strategy portfolio as enabled so it can document the full tool surface. At the default EVO_REASON_STRATEGY_MODE=off, reason_strategy is not registered at all.

What it does not claim

The most valuable documentation in this project is the part that argues against trusting it. Collected here, because a field reference that only lists capabilities is a sales page.

The gate verifies consistency, not truth

The REASON authority verifies that a conclusion follows from the premises it was given. It does not verify the truth or the provenance of those premises. Under conversational pressure the model can confabulate under induced coherence pressure — and because the verifier checks consistency with the chosen premises, a confabulation passes the gate as SOLVED.

A 28-turn stress test named five failure modes: circular premise, fact-laundering, user-premise assimilation, history confabulation, and prompted-only insight. The first mitigation was implemented and tested live, and the result is reported with unusual honesty: it forced a non-circular derivation, and “the confabulation did not disappear — it relocated”, moving the contested claim from an observation into an assumption and coining a fake epistemic kind. The conclusion recorded in the roadmap is that it is “a proven point-fix; it is insufficient alone.” The second mitigation shipped only as an advisory slice — it emits a reversal signal and does not reject the answer, pending a false-positive rate on real runs. Binding is deferred.

Triage is a planning record

The router’s determinism is downstream of a model extraction, and that extraction is the weak link. Substring provenance checks establish that a quote occurred, not that it was understood. The certificate hash identifies its contents; it does not establish their truth. A passing evaluation run is a small regression sample, not a guarantee of intent understanding.

Identity matching has a known hole

Three different normalization functions are used in different gates — normalizeExact, canonicalIdentity, and normalizeForComparison — with the result that the same drift can be tolerated by one gate and rejected by another. A fuzzy-matching second layer is designed but not implemented, and the documented decision is to keep it off the binding path until its false-accept rate has been measured.

The reviewer shares the model’s biases

Dissolution review is another call to the same configured model, not an independent verifier. It adds an explicit challenge and fails closed on missing evidence; it does not establish that all reasonable interpretations were considered.

The portfolio is unproven, and says so

The reasoning strategy portfolio defaults to off and remains gated on promotion criteria that have not been met. Seven operators are registered as unavailable. Results are scoped to a submitted finite model and never establish premise truth or model adequacy.

Formal work is integration-tested, not benchmarked

Formal recovery establishes that the mechanisms connect correctly — not that the model succeeds more often or runs faster. The constructed-proof guard is a conservative source-level check, and the project states plainly that it does not establish resistance to aliasing, tactic-generated wrappers, or semantic reformulation.