Agent Monitor provides a unified console to execute, observe, and manage informal mathematical proof runs across multiple AI engines with shared memory and tool libraries.
Proving Engines
The console offers the following proving engines. Availability depends on the deployed host. Each run receives a dedicated workspace, but local engines share the host's operating-system trust boundary rather than a hostile-code sandbox.
| Engine | Role & Architecture |
|---|---|
| Kimi proof harness | Default guest workflow: Kimi K3 drafts, critiques, and refines an argument in three tool-free stages. |
| UCLA | Multi-stage literature, advisor, solver, and verification harness. |
| IMProof | Author–Critic proving workflow based on ProofStack (improofbench). |
| Hermes | Slim embedded agent harness core (engines/hermes_core). |
| DeepAgents | LangGraph deep agent running from a dedicated Python virtual environment. |
| Meta-Harness | Harness-evolution loop (Solver $\rightarrow$ Evaluator $\rightarrow$ Proposer). |
| OpenClaw | Embedded local agent (--local). |
| External CLIs | Auto-detected coding agent CLIs (Codex, Claude Code / OpenClaude, OpenHands). Claude Code and Codex require sign-in. |
| Plain | Single-model-call baseline without additional harness scaffolding. |
Real-Time Trace Views
Monitor agent decisions, token counts, and API expenditures live using two trace views:
- Map View: A free-form, zoomable node graph where each agent node renders custom card formats depending on its action type.
- Pipeline View: A structured, fixed-stage column view displaying step-by-step progress through the proof workflow.
Persistent Library (Memory · Skills · Tools)
The 📚 Library panel allows you to store items that are materialized into _library/ and prepended as a USER LIBRARY block to agent prompts before every run:
- Memory: Context and facts saved from previous runs. Automatically generates compact summaries that can be toggled for future reuse.
- Skills: Markdown-formatted proof strategies and methods injected into agent prompts.
- Tools: Executable Bash scripts saved in
_library/tools/. CLI engines and DeepAgents can execute these scripts directly in the workspace.
Project Layout
agent_monitor/ # CLI tools, runners, and Hermes builder
monitor_core/ # Dashboard UI and token/cost tracking logic
engines/ # Vendored snapshots plus generated engine environments
problems/ # Local problem statements (UCLA, Batch-2)
data/ # Runtime runs, caches, logs, and library storeAccount boundaries
Each signed-in account owns its run history and saved provider configuration. A guest receives separate history tied to a 24-hour session cookie in that browser; clearing cookies or site data, or switching browsers or devices, loses access to it. Guest history is not transferred when the visitor later signs in. Ending the guest session deletes its saved provider keys.
Guests default to Kimi K3 with a three-stage draft → critique → refine harness. Hosted Kimi access is used when available; otherwise, guests can add their own Kimi key. The default allowance is 10 total run starts, with six starts per hour. Deleting a run does not replenish the allowance, and sign-in is required once it is used. Claude Code and Codex require sign-in from the start. Use a signed-in account for durable history, provider settings, and the other available proving harnesses.
Provider secrets saved through the console are encrypted at rest, and the normal environment for a child run is projected from the provider selected for that run. Locally executed engines remain within the host's operating-system trust boundary rather than a hostile-code sandbox. The reusable library and run workspaces remain separate concepts: library items can guide future work, while a workspace preserves the evidence and artifacts for one run.
Where to go next
- Follow the Quickstart to launch a first run.
- Choose Use as guest to try the console without an account.
- Select Sign in for durable account history.