KeyAI

verification workspace for AI research

A public map of what is proved, blocked, and still open.

KeyAI keeps formal claims, evidence, decisions, negative results, verifier outcomes, and provenance in one inspectable state. The current reference deployment is ECDLP and curve research, not an ECDLP solution.

Claim boundary No secp256k1 shortcut is claimed. The two verified ledgers remain isolated, and compiler-trusted results are labeled separately.
Browse verified results Open current research state

Reference deployment The repository demonstrates the full research-state loop on one difficult domain, but it is not yet a self-serve hosted product.

Verified research index 479 rows across 2 isolated ledgers 307 ECDLP / 172 ResearchOS / aggregate total is navigation only 0 sorry · 0 custom axioms 104 rows disclose compiler trust in ledger metadata 0 native experiments selected 1 exact synthetic-toy run completed AUTH-HYP-M16-FIXED-TARGET-YIELD-001-20260730-01
Verified results, separated by trust lane Browse theorem names, source files, proof methods, trust labels, and exact source anchors.
307
ECDLP ledger rows
~268
ECDLP distinct results
172
ResearchOS ledger rows
0 / 0
sorry / custom axioms

Evidence first

Start with the results, their limits, and the open frontier.

The public interface now exposes theorem names and exact source anchors before asking visitors to interpret the product thesis or the research workflow.

Verified result browser

479 navigation rows across two isolated ledgers, with method and trust metadata.

Browse verified results

Decision frontier

17 canonical ECDLP routes with explicit dispositions, evidence, blockers, and reconsideration triggers.

Inspect the route map

Canonical repository state

Counts, architecture, and machine-readable provenance remain generated from repository sources rather than copied into marketing prose.

Open STATUS.md Read the architecture map

The missing layer

AI can propose. KeyAI keeps the research state.

Individual agents already write proofs and code. A long research program needs a durable answer to a different question: what should the next agent trust, challenge, or stop doing?

01

Before execution

Bind each task to a source, exact scope, route, and falsifiable exit condition.

02

At verification

Record what the declared verifier accepted and what remains a semantic or empirical assumption.

03

After the attempt

Retain accepted results, negative evidence, stop conditions, and a reproducible rollback path.

Product loop

One state from source material to a governed result.

The current repository implements this loop through machine-readable contracts. The next product step is to make the same loop configurable for an external team.

01

Ingest

Pin the corpus, sources, target, and verifier contract.

02

Structure

Convert material into claims, dependencies, barriers, and threat models.

03

Decide

Select, park, or reject routes under explicit evidence gates.

04

Execute

Give a human or model one bounded task with a falsifiable exit condition.

05

Verify

Run the declared verifier and an independent result validator where needed.

06

Retain

Promote accepted results and preserve negative evidence, provenance, and rollback.

Active validation / TASK-011

The next result must come from another team.

We are recruiting one formal-research team to test the current workspace, map one repeated workflow, and make an evidence-based build, change, stop, or pending decision.

Status
recruiting
Session
60 minutes
Completed discovery
0 sessions
Read the pilot contract Apply on GitHub

Reference deployment

A difficult research boundary, represented honestly.

secp256k1 is the test case, not the product claim. It forces KeyAI to distinguish a theorem, an experiment, a threat model, a failed route, and a practical attack.

Current route decision

RS-2026-07-24-001 · 2026-07-24

Monitoring
SELECT_NONE

No current route clears the proposal gate.

Completed the bounded, non-experimental GLV-SEMAEV-ITER-001. Only the diagonal C3 scalar polynomial covariance survives for S3 and S4; the naive independent-cube premise and the S4 fixed-target coordinate-scaling premise are bounded negatives. The S4 certificate isolates r=0, and Lean proves that no F_p-rational affine secp256k1 target inhabits that slice. No route or hypothesis is promoted, no solver run is authorized, and the primary ECDLP objective remains unchanged.

  • RS-2026-07-22-001 is historical after supersession; this current decision explicitly carries forward its zero-promotion assessment.
  • The owner selected the exact S3/S4 coordinatewise C3 polynomial classification and the S4 fixed-target consequence as the sole current structural uncertainty because they can resolve the premise of the naive GLV-Semaev quotient without an attack run.
  • Exact symbolic certificates and narrowly scoped Lean covariance theorems can reduce this uncertainty while preserving the parked experiment status and every P0-P4 result.

Inspect all 17 route dispositions

What exists now

Evidence, not a product demo made of placeholders.

Each capability below links to a live artifact in the reference repository.

Kernel-checked result ledger

Inspectable in the reference repository and checked by the repository gates.

VERIFIED.md

Tasks, hypotheses, graph, provenance, and generated views

Inspectable in the reference repository and checked by the repository gates.

tasks/NEXT.md

Current capability

Reference system

  • Kernel-checked result ledger
  • Evidence-gated route decisions
  • Reproducible candidate and independent validation contract
  • Tasks, hypotheses, graph, provenance, and generated views

Not yet

Hosted product

  • Self-serve repository or corpus import
  • Hosted multi-project workspaces
  • Authentication, collaboration, and organization controls
  • A verifier adapter beyond the current repository contracts
  • Validated external users, retention, or willingness to pay

The next product milestone

We will call it an MVP when another team can run the loop.

A non-owner research team can connect a second project, obtain a trustworthy initial map, run one candidate through its verifier, and understand the resulting decision without editing KeyAI's generator code. A technical MVP still does not establish a repeatable buyer or willingness to pay.

orientation-time

A new collaborator identifies current state, blockers, and next action in 10 minutes or less.

provenance-completeness

Every promoted result links to its source, task, verifier result, and trust boundary.

state-drift

Zero stale generated or public artifacts after a canonical state change.

external-pilot

At least one external team completes the core loop and returns for a second session.