# Harmonic

**Canonical:** https://apis.io/providers/harmonic/  
**Website:** https://www.harmonic.fun  
**APIs profiled:** 1

Harmonic is a Palo Alto AI lab building Mathematical Superintelligence (MSI) — AI that reasons with rigorous, verifiable logic rather than statistical pattern matching. Its flagship product, Aristotle, is a formal reasoning agent that uses Lean 4 to prove and formally verify graduate- and research-level problems in mathematics and software. Developers access Aristotle through the Aristotle API (https://aristotle.harmonic.fun) and the official Python SDK/CLI (aristotlelib): submit Lean 4 proof files with `sorry` placeholders, plain English math problems, or LaTeX research papers, and Aristotle attempts to complete, formalize, and formally verify them — running autonomously for up to 24 hours on larger tasks and returning only formally checked results. Harmonic was co-founded by Vlad Tenev (co-founder of Robinhood) and Tudor Achim, and is backed by Kleiner Perkins.

## Kin Score — 22.4 / 100 (emerging)

Scored 2026-08-30 under rubric 0.17.2. Trend: flat (+0.0 from 22.4).

| Facet | Score |
|---|---|
| Discoverability | 68.5 |
| Contract Quality | 0.0 |
| Governance | 0.0 |
| Contract Governance | 0.0 |
| Operational Transparency | 18.4 |
| Developer Ergonomics | 38.1 |
| Commercial Clarity | 27.6 |
| Access Clarity | 27.6 |

## Agent readiness — 6.0 (agent-aware)

| Dimension | Value |
|---|---|
| Spec Presence | no |
| Agentic Access | no |
| Reversibility Documented | no |
| MCP Server | documented |
| Auth Clarity | bearer |
| Idempotency | no |
| Error Semantics | no |
| OpenAPI Examples | no |
| Rate Limit Signal | no |
| Event Surface Described | no |
| Agent Skills | no |
| Well Known Catalog | no |
| Consent Identity | no |
| Agent Card | no |
| Dry Run Mode | no |
| Delegated Identity | no |
| Protected Resource Metadata | no |
| Dynamic Client Registration | no |
| Agentic Commerce | no |

## Access

Self-serve signup — onboarding: self-serve, pricing: unknown, trial: no (confidence: medium).

## APIs (1)

- **Aristotle API** — Programmatic access to Aristotle, Harmonic's formal reasoning agent. Over HTTPS with an API key, submit Lean 4 proofs with `sorry` placeholders, natural-language math problems, ...

## MCP servers (1)

- **Harmonic MCP Server** — Harmonic does not (as of this pass) publish an official MCP server for the Aristotle API. A working community MCP server, lean-aristotle-mcp (maintained by GitHub user septract)...

## Security (2)

- **Harmonic Authentication** — apiKey · 1 scheme
- **Harmonic Domain Security** — TLSv1.2 · DMARC

## Tags

Company, Artificial Intelligence, Mathematics, Formal Verification, Theorem Proving, Lean, Machine Reasoning, Developer Tools

---

Profiled by [API Evangelist](https://apievangelist.com) and published on [APIs.io](https://apis.io/providers/harmonic/). Scores are computed from the provider's own public artifacts under a published rubric.