Exit code 0 answers one narrow question: did the child process report an operating-system failure? It does not say that MiniZinc produced a complete solution, that the output belongs to the input we sent, or that an award is safe to persist.
That distinction shaped the clearing boundary in Freight Capacity Auction Clearing Engine. The worker is allowed to run an optimizer. It is not allowed to treat the optimizer as an authority. Before an award enters PostgreSQL, the system needs a configured backend, a normalized version, canonical input and output hashes, a parsed terminal status, and a decision record for every awarded, rejected, or unassigned load.
A clean process exit is only one piece of that evidence.
Process success and freight success are different facts
The tempting implementation is short. Spawn MiniZinc, wait for exit code 0, decode whatever JSON arrived on stdout, then write the selected bids. That design works while every solver run is polite. It fails at the boundary cases that matter most: truncated output, duplicated final records, a terminal status followed by another parsed solver record, an executable that reports a version but lacks the expected capability, or a timeout that leaves descendants alive.
None of those cases should produce a freight commitment.
I split the responsibility across three modules. Process_runner owns the child process. It receives one executable and literal arguments, never a shell command. It bounds stdin, stdout, and stderr independently, applies a deadline, captures typed exit outcomes, and cleans up the process tree. Solver_backend owns health probing and terminal output grammar. Solver_execution joins those pieces and refuses output that lacks the domain status.
The distinction is visible in the types. Process_runner may return Success because the executable exited normally. Solver_backend.parse_minizinc_stream can still return Malformed_output. The latter decision wins.
I was wrong to treat process success as solver success. The tests made the gap concrete. A fixture can emit plausible JSON, exit 0, and omit the terminal status. Another can emit the terminal status twice. Both look healthy if the adapter checks only the process outcome. Neither is a valid clearing result.
One terminal record, exactly once
The parser is small because its contract is narrow. This is the production code from src/solver/solver_backend.ml, lines 353-371:
let parse_minizinc_stream value =
let lines =
String.split_on_char '\n' value
|> List.filter (fun line -> String.trim line <> "")
in
let is_separator line =
let line = String.trim line in
line <> "" && String.for_all (function '-' | '=' -> true | _ -> false) line
in
let rec loop seen_status = function
| [] -> (match seen_status with Some status -> Ok status | None -> Error Malformed_output)
| line :: rest ->
(match parse_line line with
| Some (`Terminal status) -> (match seen_status with None -> loop (Some status) rest | Some _ -> Error Malformed_output)
| Some `Other -> (match seen_status with None -> loop seen_status rest | Some _ -> Error Malformed_output)
| None when is_separator line -> loop seen_status rest
| None -> loop seen_status rest)
in
loop None lines
The parser accepts ordinary solver records before the terminal record. After terminal status, another parsed solver record is malformed, and a second terminal status fails for the same reason. MiniZinc separators and unrecognized lines are tolerated on either side of the terminal record, but they don't count as evidence. Reaching the end without a status is malformed.
This rule covers SATISFIED, OPTIMAL_SOLUTION, ALL_SOLUTIONS, UNSATISFIABLE, UNBOUNDED, UNSAT_OR_UNBOUNDED, UNKNOWN, and ERROR. The important part is not which words are accepted. It is that the worker receives one explicit end state rather than guessing from silence.
The next layer maps a malformed stream to the stable code SOLVER_OUTPUT_INVALID. In bin/worker.ml, the same failure becomes a job error stating that the solver failed before producing terminal evidence. No award persistence runs after that branch.
The child process cannot own the boundary
Terminal parsing would be weak if the process adapter could leak resources or accept hostile command construction. The shared runner therefore keeps executable and arguments separate. It rejects NUL-bearing input before spawn, including a leading NUL that has special meaning in the Lwt process implementation on Windows. Environment names are allow-listed by the caller. There is no string command API.
Output is bounded too. The solver execution path allows up to 1 MiB on stdout and 64 KiB on stderr. Those are operational caps, not optimization parameters. A solver that floods either stream should fail as a process boundary violation, not consume memory until the worker becomes unstable.
Timeout and cancellation share the same cleanup path. On POSIX, the child runs in a private process group. The runner sends a termination signal, allows a bounded grace period, checks whether the group remains, sends a kill signal when needed, reaps the leader, and verifies group absence. The test fixture covers a child whose leader exits while a descendant resists termination. That is an ugly case, and it is exactly why process control lives below the solver adapter.
Windows cleanup is recorded as unproven by the fixture. The code returns a typed termination-unavailable result when it cannot prove cleanup. I would rather carry that gap in the release record than turn POSIX evidence into a cross-platform claim.
Evidence must survive the worker
Parsing one terminal status stops malformed output, but it does not bind the result to the auction. The worker still has to preserve what was solved.
Before execution, it builds canonical JSON from sorted loads and bids. Stable ordering matters because the same freight facts should produce the same input hash regardless of database retrieval order. The worker probes the selected backend, records its normalized version, and hashes the canonical input. After execution, it hashes the output artifact. The configured backend never changes automatically. If MiniZinc is selected and missing, an available OR-Tools binary does not quietly take over.
That no-fallback rule costs availability. It also keeps the evidence honest. A replay or operator can tell which optimizer produced the decision. Silent fallback would make a job look continuous while changing the model, solver behavior, or explanation surface underneath it.
The persistence boundary then writes the job state, solver identity, hashes, award rows, and clearing decisions in PostgreSQL. The release fixture expects both positive and negative decisions. One bid wins; the other remains a rejected decision with its reason. Saving winners alone would make the optimizer look decisive while deleting the evidence needed to explain competition.
Clearing_service.clear adds the final guard. If solver evidence is absent, it returns an infeasible result with SOLVER_EVIDENCE_REQUIRED. Policy filtering can reject bids above reserve, below service requirements, or beyond carrier-share limits. Scoring can rank eligible bids. None of that logic may bypass the evidence requirement in production clearing.
What surprised me about malformed success
I expected the hardest solver tests to be about objective values and capacity constraints. The sharper tests were about output shape.
The canonical fixture has four loads, four carriers, eight eligible bids, and three excluded bids. It produces eleven decisions and resolves a score tie by UUID. Those checks matter because deterministic explanations depend on them. But the fixture that changed my view is smaller: valid-looking output with no terminal status. It proves that a solver adapter can parse useful lines, receive exit code 0, and still have no right to persist the answer.
That failure is dangerous because it resembles success. The process finished. The logs may show no crash. Some assignments may already be present in stdout. An adapter that accepts partial output can create a complete-looking award from an incomplete run.
The same reasoning applies after solving. An award that requires approval stays non-exportable. The local release lifecycle submitted two bids, persisted one award and one rejection with solver hashes, then received HTTP 409 when it requested export before approval. After approval, the export returned HTTP 200 from a frozen snapshot. Solver success did not grant export authority. Approval did.
These are separate gates on purpose. Process execution says the program ran. Terminal evidence says the solver declared an end state. Persistence says the decision and its proof were written together. Approval says a person accepted the operating consequence. Export says the accepted record can leave the system without changing later.
What the local proof says, and what it does not
On 27 August 2026, the local release gate passed the OCaml unit suite, PostgreSQL 16 and Redis 7 integration suites, Dream lifecycle checks, hostile child-process fixtures, MiniZinc artifact tests, DuckDB and Parquet checks, browser journeys, and the packaged Docker lifecycle.
The solver fixture covered optimal, satisfied, infeasible, unbounded, unknown, error, timeout, nonzero exit, and malformed stream cases.
That is measured local validation. It is not production throughput, live carrier behavior, or proof that the larger PRD targets have been met. The published system supports one production clearing mode, single_round_spot. Other auction modes remain explicit unsupported cases. External notification and workflow delivery also remain outside the local proof.
The transferable point is narrow: an optimization result needs a domain completion record, not just a successful process. If the boundary cannot prove which solver ran, what it saw, how it ended, and what it wrote, exit code 0 is administrative trivia.
