Harmonic

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.

Harmonic publishes 1 API on the APIs.io network. Tagged areas include Company, Artificial Intelligence, Mathematics, Formal Verification, and Theorem Proving.

Harmonic’s developer surface includes signup flow, engineering blog, authentication, CLI, changelog, and 13 more developer resources.

🌐 Visit website 📡 Source on GitHub

22.4/100 emerging ▬ flat Agent 6/100 agent aware saas Full breakdown ↓
scored 2026-08-30 · rubric v0.17.2

AccessSelf serve

1 APIs 1 MCP Servers

Company Artificial Intelligence Mathematics Formal Verification Theorem Proving LeanMachine ReasoningDeveloper Tools

Kin Score

Kin Score How this is scored →
scored 2026-08-30 · rubric v0.17.2

Composite quality — 22.4/100 · emerging

Contract Quality 0.0 / 25

Developer Ergonomics 7.6 / 20

Access Clarity 5.5 / 20

Operational Transparency 2.4 / 13

Contract Governance 0.0 / 12

Discoverability 6.9 / 10

Agent readiness — 6/100 · agent aware

Machine-Readable Contract 0 / 18

Agentic Access Contract 0 / 10

Documented Reversibility 0 / 6

MCP Server 12 / 12

Machine-Readable Auth 10 / 10

Idempotency 0 / 9

Stable Error Semantics 0 / 8

Request/Response Examples 0 / 7

Rate-Limit Signaling 0 / 7

Typed Event Surface 0 / 6

Agent Skills 0 / 5

Well-Known Catalog 0 / 4

Consent & Bot Identity 0 / 3

A2A Agent Card 0 / 8

Dry-Run / Simulate Mode 0 / 4

Delegated User Identity 0 / 6

Protected Resource Metadata 0 / 5

Registration Without a Human 0 / 6

Agentic Commerce Surface 0 / 5

Improve this rating by publishing the missing artifacts — every area above can be raised, and the full rubric is at apis.io/rating/. This rating is computed from github.com/api-evangelist/harmonic: open an issue to ask a question, or submit a pull request to add artifacts. Want it done for you? Prioritized profiling — $2,500 →

APIs 1

Individual APIs this provider publishes, each with its own machine-readable definition.

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

Model Context Protocol servers that expose these APIs to AI agents.

Get Started 3

Portal, sign-up, and the first successful call

DeveloperPortal

DeveloperPortal

SignUp

SignUp

Login

Agent Surfaces 2

MCP servers, agent skills, and machine-readable catalogs

MCPServer

MCPServer

LLMsTxt

LLMsTxt

Design & Contract 2

Pagination, idempotency, versioning, errors, and events

Conventions

Conventions

Lifecycle

Lifecycle

Build 4

SDKs, sample code, and the tooling you integrate with

GitHubOrganization

Packages

SDKs

CLI

Access & Security 2

Authentication, authorization, and security posture

Authentication

Authentication

DomainSecurity

DomainSecurity

Operate 1

Status, limits, changes, and where to get help

ChangeLog

ChangeLog

Commercial 2

Pricing, plans, and the legal terms of use

TermsOfService

TermsOfService

PrivacyPolicy

PrivacyPolicy

Company 2

The organization behind the API

Website

Website

Blog

Blog

Source (apis.yml)

aid: harmonic
name: Harmonic
description: '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.'
url: https://raw.githubusercontent.com/api-evangelist/harmonic/refs/heads/main/apis.yml
x-type: company
x-source: kleiner-perkins-portfolio
x-tier: enriched
x-tier-reason: portfolio-lead
deliveryModel:
  model: saas
  open_source: false
  commercial: true
  callable_host: false
  label: Hosted service · you call their endpoint
  confidence: medium
  source:
  - pricing
  generated: '2026-08-28'
  method: derived
accessModel:
  pricing: unknown
  onboarding: self-serve
  trial: false
  try_now: false
  public: false
  label: Self-serve signup
  confidence: medium
  source:
  - authentication
  generated: '2026-07-22'
  method: derived
specificationVersion: '0.23'
image: https://www.harmonic.fun/images/harmonic-blue.svg
created: '2026-07-17'
modified: '2026-07-19'
tags:
- Company
- Artificial Intelligence
- Mathematics
- Formal Verification
- Theorem Proving
- Lean
- Machine Reasoning
- Developer Tools
tags_raw:
- Company
- Ai
- Mathematics
- Formal Verification
- Theorem Proving
- Lean
- Machine Reasoning
- Developer Tools
apis:
- name: Aristotle API
  description: 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, or LaTeX papers; Aristotle fills sorries, formalizes
    documents into Lean 4, and returns only formally verified results. The API is asynchronous — submit a job and poll/download
    the result — and is driven primarily through the official aristotlelib Python SDK and `aristotle` CLI.
  humanURL: https://aristotle.harmonic.fun
  baseURL: https://aristotle.harmonic.fun
  tags:
  - Formal Verification
  - Theorem Proving
  - Lean
  - Mathematics
  properties:
  - type: SignUp
    url: https://aristotle.harmonic.fun/auth/login?screen_hint=signup
  - type: Login
    url: https://aristotle.harmonic.fun/auth/login
maintainers:
- FN: Kin Lane
  email: kin@apievangelist.com
- FN: APIs.json
  email: info@apis.io
common:
- type: Website
  url: https://www.harmonic.fun
- type: DeveloperPortal
  url: https://aristotle.harmonic.fun
- type: SignUp
  url: https://aristotle.harmonic.fun/auth/login?screen_hint=signup
- type: Login
  url: https://aristotle.harmonic.fun/auth/login
- type: TermsOfService
  url: https://aristotle.harmonic.fun/terms
- type: PrivacyPolicy
  url: https://aristotle.harmonic.fun/privacy
- type: Blog
  url: https://harmonic.fun/news
- type: GitHubOrganization
  url: https://github.com/harmonic-ai
- type: Authentication
  url: authentication/harmonic-authentication.yml
- type: Packages
  url: packages/harmonic-packages.yml
- type: SDKs
  url: packages/harmonic-packages.yml
- type: CLI
  url: cli/harmonic-cli.yml
- type: MCPServer
  url: mcp/harmonic-mcp.yml
- type: LLMsTxt
  url: llms/harmonic-llms.txt
- type: Conventions
  url: conventions/harmonic-conventions.yml
- type: ChangeLog
  url: changelog/harmonic-changelog.yml
- type: Lifecycle
  url: lifecycle/harmonic-lifecycle.yml
- type: DomainSecurity
  url: security/harmonic-domain-security.yml
x-enrichment:
  date: '2026-07-19'
  status: backfilled
  pass: local-v1
  note: backfilled from .gitignore signal + verified work evidence

Work with this as data

Every provider here is available over the APIs.io API and to AI agents over MCP.

MCP server

One button, every client — Claude, Cursor, VS Code and the rest.

https://apis.io/mcp

Tools for providers

9 MCP tools reach this

find_providersBrowse and filter every provider in the catalog.
get_provider_artifactsEvery artifact this provider publishes, grouped by type.
get_provider_operationsEvery operation across all of their OpenAPIs — one call instead of parsing every spec.
get_provider_toolsEvery MCP tool they ship, with the operation each wraps.
get_provider_evidenceHow each part of their score was established. Free — the basis for a claim should not sit behind it.
get_provider_ratingPRO — composite, band, trend and facet scores.
apis_io_searchSTART HERE — APIs, providers and tags for one query, each with its total.
resolveTurn a domain, URL or GitHub org into the provider it belongs to.
find_cohortsEvery scored population of providers in the catalog.

All 92 tools →

Call it yourself

curl for this page

This provider

curl "https://apis.io/api/v1/providers/harmonic"

All providers

curl "https://apis.io/api/v1/providers?limit=25"

Every operation they expose

curl "https://apis.io/api/v1/providers/harmonic/operations?limit=25"

How their score was established

curl "https://apis.io/api/v1/providers/harmonic/evidence"

Discovery needs no key. Ratings and market analysis are Pro.

Get an API key

Free tier, no email required.

GitHub Google LinkedIn

A second provider on the same verified email joins the account you already have.