TEKMERION: Proof Surface Compiler

TEKMERION reveals when “approval” and “success” logs cannot prove an agent executed what a human authorized, then compiles the missing evidence into a reviewable patch and deterministic check.

Comment

Inspiration

Agentic systems are increasingly allowed to deploy code, change infrastructure, publish content, transfer assets, or modify production resources after a human approval step.

Yet most audit trails record only that:

  • an approval occurred;
  • an executor was called;
  • the operation returned success.

Those events prove activity. They do not prove that the action reaching the real tool was the action the human approved.

TEKMERION began with a simple thesis:

Many operational guarantees are not only violated. They are untestable because the system never preserved the evidence required to evaluate them.

The answer is not to log everything. It is to identify the specific evidence and deterministic relationships required by a specific operational claim.

What it does

TEKMERION is a Proof Surface Compiler for agentic workflows.

Given an operational guarantee and a bounded workflow, it:

  1. creates matched compliant and violating executions;
  2. tests whether the current telemetry can distinguish them;
  3. uses GPT-5.6 to compile a structured candidate evidence plan;
  4. maps evidence requirements to real repository symbols and execution boundaries;
  5. uses Codex to materialize a reviewable instrumentation and verification patch;
  6. evaluates the resulting evidence with deterministic code.

The reference workflow is a simulated production deployment with human approval.

Both the compliant and altered executions initially report:

  • approval received;
  • executor called;
  • deployment succeeded.

The baseline telemetry therefore cannot establish whether the action received by the actual tool still matches the approved action.

The current MVP fully materializes and validates one proof slice:

Action equivalence: the executed action must match the approved action.

With the selected evidence installed:

  • a compliant execution is deterministically accepted;
  • a post-approval manifest drift is deterministically detected.

GPT-5.6 also produced a broader candidate plan for approval identity, session binding, workflow binding, relevant state, freshness, and single use. That wider plan is shown as a candidate—not as a completed proof surface.

How we built it

TEKMERION is a TypeScript monorepo with separate packages for:

  • workflow simulation;
  • telemetry and normalization;
  • deterministic proof predicates;
  • scenario generation;
  • GPT-5.6 claim compilation;
  • web-based judge replay.

The scenario engine contains 12 matched compliant/violating pairs across four fault families:

  • manifest drift;
  • claim-relevant state drift;
  • replay, session, and freshness failures;
  • actual tool-argument mutation.

That produces 24 deterministic executions. Under generic baseline telemetry, every matched pair remains observationally equivalent for the bounded claim.

The GPT-5.6 compiler uses the OpenAI Responses API with strict structured output. It receives:

  • the operational guarantee;
  • canonical obligation, probe, and predicate registries;
  • an allowlisted symbol index;
  • bounded repository excerpts;
  • explicit privacy and authority constraints.

GPT-5.6 returns a structured candidate plan containing:

  • obligation-to-predicate mappings;
  • recommended evidence probes;
  • predicate dependencies;
  • repository code mappings;
  • rejected alternatives;
  • assumptions and limitations.

The model is not allowed to issue the final verdict, redefine deterministic policy, select global minimality, or generate unrestricted code.

A deterministic assembler and semantic validator hydrate canonical definitions, enforce symbol and path policies, reject unsafe proposals, and preserve provenance.

For the validated action-equivalence slice, TEKMERION captures session-scoped keyed evidence independently at:

  • the approval boundary;
  • the actual tool boundary.

A deterministic predicate then compares both observations within the same digest context.

The repository also includes an exact selector-mechanics test in a bounded toy universe. It exhaustively evaluates eight subsets and retains the complete class of two equal-primary-cost optima. This validates dependency closure, coverage, lexicographic cost, and deterministic tie-breaking, but it is intentionally kept separate from the validated A04 proof slice.

Judge mode is deterministic, recorded, and requires no OpenAI API key or outbound network access.

How GPT-5.6 and Codex were essential

GPT-5.6

GPT-5.6 is part of the product, not only a coding assistant.

It translated the operational guarantee into a non-trivial candidate evidence plan that mapped seven obligations to:

  • bounded probes;
  • deterministic predicates;
  • concrete repository symbols;
  • safe instrumentation boundaries;
  • rejected privacy-invasive alternatives.

The reviewed proposal rejected raw prompts, raw action manifests, full state snapshots, stable cross-session hashes, and additional generic status logging.

GPT-5.6 proposes what evidence may be required. It does not grade its own proposal.

Codex

Codex was the primary implementation collaborator and patch materializer.

It helped build:

  • the deterministic workflow simulator;
  • the 12-pair scenario catalog;
  • ground-truth isolation;
  • telemetry normalization;
  • the structured GPT-5.6 compiler;
  • semantic safety policies and quarantine;
  • the approval/tool-boundary evidence patch;
  • deterministic predicates;
  • privacy, integration, isolation, and reproducibility tests;
  • the local judge replay and Compiler Workbench.

Product scope, model authority, privacy boundaries, formal semantics, human review, and final acceptance decisions remained human-controlled.

Challenges we ran into

Separating truth from evidence

The experiment must know whether an execution is compliant or violating, but the verifier must not see scenario labels, injected faults, or expected outcomes.

We created strict boundaries between:

  • experiment ground truth;
  • retained telemetry;
  • deterministic verifier input.

Tests fail if control-plane information leaks into the evidence path.

Making GPT-5.6 useful without letting it self-grade

The model needed enough semantic freedom to map a human guarantee to code, while deterministic software retained authority over:

  • schemas;
  • allowed symbols;
  • dependency closure;
  • coverage;
  • selection;
  • path policy;
  • final verdicts.

At one point, a valid GPT-5.6 proposal was quarantined because a negative privacy statement mentioned “raw prompts.” We made the policy field-aware, preserved the unchanged proposal, and promoted it only after human and deterministic validation.

Avoiding “log everything”

Raw prompts and complete manifests would make comparison easy, but would weaken the privacy thesis.

The validated slice instead uses bounded canonical projections and session-scoped keyed digests. Raw prompts and raw action manifests are not retained in the proof evidence.

Staying honest about scope

The broader A01–A07 plan is a candidate plan. The action-equivalence slice is validated. Selector mechanics are tested separately in a toy universe. Held-out validation and the complete hero surface remain future work.

Those statuses are deliberately distinct in the interface.

Accomplishments that we are proud of

  • A real GPT-5.6 product call produced a structured, reviewed candidate evidence plan.
  • The proposal maps operational obligations to concrete source symbols instead of returning generic advice.
  • Twelve matched scenario pairs produce 24 reproducible executions across four fault families.
  • Generic baseline telemetry remains unable to distinguish the compliant and altered executions.
  • The validated A04 slice changes that capability: compliant execution passes and manifest drift fails.
  • Codex materialized a real, human-reviewed instrumentation and verification patch.
  • The final verdict is deterministic, not model-generated.
  • Judge replay requires no API key, database, Docker environment, or external service.
  • The selected evidence retains no raw prompts or raw action manifests.
  • The repository includes strict schema, privacy, isolation, provenance, reproducibility, and secret-scanning controls.

What we learned

The most important lesson was:

More observability does not automatically create more knowledge.

A log line is useful only when it participates in a relationship that can evaluate the claim.

We also learned that probabilistic models and deterministic software are strongest when they have different responsibilities:

  • GPT-5.6 performs semantic compilation;
  • Codex materializes reviewable implementation;
  • humans approve consequential decisions;
  • deterministic code evaluates the evidence.

Finally, evidence minimization is not only an optimization problem. It is a privacy and accountability design principle.

What’s next for TEKMERION

The next technical milestone is to complete selection and validation for the wider candidate plan:

  • approval identity, session, and workflow binding;
  • claim-relevant state compatibility;
  • approval freshness;
  • single-use and replay prevention.

Future work also includes:

  • held-out scenario validation;
  • ablation and overhead measurement;
  • complete full-catalog proof-surface selection;
  • adapters for bounded external repositories;
  • a CLI and GitHub Action for CI claim regression;
  • stronger evidence-integrity and attestation mechanisms.

The long-term vision is a developer tool that turns operational responsibilities into maintained, machine-checkable evidence contracts.

TEKMERION did not add more telemetry. It added the evidence the claim required.

Built With

Share this project:

Updates