Echea

Superintelligence Research Lab at the Frontier of Deterministic Algorithms

General: LLM Design: Chip Design:

Copied

A New Paradigm

Formal Reasoning for Verifiable AI

Formal Reasoning for Exact AI

We are building faster SAT logic solvers: deterministic algorithms for structured NP-Complete problems at industrial scale.

Formal reasoning and mathematics can produce more exact, verifiable, and cost-efficient answers in large combinatorial spaces where the structure is present.

Less trial-and-error. More deduction where deduction is possible.

Today's AI systems are powerful, but they remain expensive, approximate, and difficult to verify.

Echea treats hard problems as sets of constraints to solve and optimize. Chip layouts, trades, molecules, and model-training decisions can all be written as constraints: what must be true, what cannot happen, and what should be maximized.

Once a system is expressed that way, formal reasoning can search for exact answers with clearer verification paths and lower trial-and-error cost. Everything is a constraint system if you choose the right representation.

NP-Completeness

One Problem Class. Every Industry.

Shared Optimization Across Industries

Chip placement, supply chain routing, molecular search, order scheduling, and parts of neural-network training can be framed as hard combinatorial problems. Similar search structures appear across many critical systems.

We are building a general API and MCP layer that exposes more exact, deterministic algorithms for this shared problem class. One technical foundation can serve several industries because the underlying optimization patterns often repeat.

Chip layouts, supply chains, molecule searches, trading portfolios, and parts of AI training contain related classes of hard optimization problems.

We are building a general API layer for these problems. Chip designers send layouts, quant firms send order books, and pharma teams send molecular spaces. Each customer receives a more exact, auditable answer for a related mathematical problem class.

This creates one technical foundation with multiple high-value commercial markets.

Scaling Laws

SAT Scaling Laws

Recursive Algorithmic Improvement

Two scaling laws define the trajectory of AI: deterministic (Algorithms) and empirical (Data+Compute+Algorithms).

SAT solvers themselves have gotten roughly 10,000× faster since the 1980s driven by algorithmic breakthroughs. Yet empirical scaling has still outpaced that curve for the last Two decades. The deterministic curve can be measured and improved: each generation of the algorithm can be benchmarked, verified, and refined with less stochastic variance than empirical scaling.

Recursive stochastic superintelligence improves asymptotically: more data, more samples, closer approximations.

Deterministic reasoning targets the exact optimum. The deterministic solution is perfect optimization, with a result that can be measured, verified, and improved.

Echea is building on that curve.

The Hardest Problems

Beyond Gradient Descent

Limits of Stochastic Training

The industry settled on a training paradigm that works. The first paradigm was about getting something to work. The next is about finding out why it works. One must just look in the right places.

Guesswork and Approximation.
Messy and Expensive.

Gradient descent is a step by step method.
Time must be used.

But why not simultaneously?

Modern AI training relies on stochastic search through a vast parameter space.

The process requires billions of incremental updates and large amounts of compute, often producing a useful model without a direct proof that the search path was optimal.

Echea targets the mathematical structure beneath this search process, reducing reliance on trial-and-error with deterministic reasoning where the problem structure allows it.

The Frontier Paradigm Shift

The Middle Ground

Formal Methods for Model Training

AI has long swung between two poles: symbolic AI, rule-based and deterministic but brittle at scale, and stochastic AI, powerful but probabilistic and difficult to verify.

We are pursuing the middle ground. Formal reasoning does not need to replace neural networks; it can help train and verify selected parts of them.

Today's AI. Effective, but approximate, expensive, and difficult to verify.

Echea. Deterministic algorithms that can make selected parts of model training more exact, efficient, and mathematically auditable.

The objective is not to replace neural networks, but to train them with stronger mathematical checks where the structure allows.

Becoming a Frontier Lab Algorithm · Software

Pre-Training Reversed

Model Training

We investigate a reverse view of gradient descent. Rather than only descending toward a minimum, we specify a target loss L* and search for inputs or weights that can reach it with less stochastic waste.

Standard training moves through many small optimization steps, consuming substantial compute before arriving at a useful model.

Echea investigates the reverse problem: specify a target loss or model quality, then solve for the inputs or weights that reach it. This reframes training as a direct optimization problem rather than a long stochastic walk.

Optimization as a Service Compute · Hardware

Chips Perfected

Exact Silicon Optimization

We target placement and routing at silicon scale, packing billions of transistors into less area while finding stronger signal routes across metal layers.

Advanced chip layout is a high-value optimization problem with billions of placement and routing decisions. Current tools rely heavily on heuristics and can leave meaningful area and routing efficiency unrealized.

Echea applies deterministic solvers to improve placement, routing, and silicon utilization with more verifiable search. On a $300M tape-out, even a 3% improvement represents $9M in value before recurring gains across future chip families.

Publications

Research & Theory

Research and Technical Work

A growing library of the publicly released papers that document our work on formal reasoning, deterministic algorithms, and the mathematical foundations of verifiable AI systems.

Public papers and technical memos documenting the mathematical basis of Echea's deterministic reasoning systems.

Appendix

Team

Jonathan Belay

Founder & CEO

Harvard CS '22. Founder of the first AI club at Harvard. Google Connectomics team, pre-training.

Simeon Radev

Co-Founder & CTO

Harvard CS '22. MIT for AI on NP-Complete protein folding. Etched for NP-Complete chip design.

William Shen

Biopharmaceutical Advisor

Harvard MCB '22. Harvard Med for NP-Complete drug design.

Henry Bosch

Mathematical Advisor

Harvard CS '22. Stanford PhD in Math & CS. Etched for NP-Complete chip design. Lead Organizer of the Stanford PhD Seminar on Math & Computation.

Appendix

Academic Mentor

The leading expert researcher in our domain of computational complexity (#P Completeness), machine learning theory, and the mathematical foundations of computing.

Leslie Valiant

Turing Award Laureate · T. Jefferson Coolidge Professor of Computer Science and Applied Mathematics, Harvard University

He advises us informally and stays engaged with our theoretical progress.

Appendix

Go-to-Market Strategy

Chip design is our focus. That is where even a measured speed or quality improvement can be worth the most today, and where our first commercial contract is targeted. Quant trading and pharma are adjacent markets we expand into once the chip-design solver is in production.

01
Priority · Now
Chip Design, Placement & Routing

Land with a top-5 fabless semiconductor customer; augment existing EDA workflows on advanced nodes where even small area, power, or routing improvements have high dollar value.
02
Down the Line
Quant Trading, Order Scheduling

Partner with a tier-1 systematic trading firm to make order-routing and execution scheduling more auditable, where deterministic checks can support both regulatory review and performance.
03
Down the Line
Pharma, Molecular Optimization

Apply deterministic combinatorial search to protein folding and drug target discovery pipelines, where more exact search can reduce trial-and-error cycles and experimental cost.

Target partners LOI TBD

Appendix

Product & Pricing

01

API Access

Per-solve pricing against a committed spend floor. Anchor customers commit $100K to $500K per year. Right tier for pilots, smaller workloads, and adoption inside customer R&D teams.
02

Enterprise License

Annual contract for unlimited production use. Target range: $1M to $10M per year, sized by customer scale and call volume. This is where most beachhead revenue will sit.
03

Embedded Solver

Integrated into customer infrastructure for silicon-scale call volume. Multi-year contracts, $5M to $25M, reserved for the largest customers running production workloads at scale.

Top-5 fabless tape-outs can run $100M to $500M+. If deterministic placement-and-routing can recover even a few points of area, power, or routing efficiency, a 3% improvement on a $300M tape-out represents $9M of potential value per family before recurring gains.

Appendix

Market Size

SAT solvers have become roughly 10,000× faster from the 1980s to today driven by algorithmic breakthroughs, not Moore's Law. That curve hasn't flattened. Each new order of magnitude unlocks a potentially larger market.

SOM · 10× + Tooling $10B

SAT + CUDA-style dev platform

A 10× SAT solver plus a CUDA-style developer ecosystem could serve formal verification, EDA, and constraint-programming tooling.

SAM · 100× Faster $200B

Combinatorial optimization × ML

100× speedups could open larger parts of the combinatorial-optimization stack: scheduling, routing, and discrete optimization inside machine learning.

TAM · 10,000× Faster $2.5T+

Reducing stochastic search cost

At very large speedups, deterministic solvers could reduce the AI infrastructure spend currently consumed by stochastic search.

Appendix

Competitive Landscape

The research lab landscape is splitting along two dimensions: stochastic versus deterministic (formal reasoning), and specific systems versus general intelligence. Echea sits in the top-right: general formal reasoning for exact optimization.

Stochastic

Deterministic (Formal Reasoning)

General

Specific

Echea Harmonic Math, Inc. Axiom Math CTGT Ricursive Chips Recursive Unconventional AI Anthropic OpenAI Google DeepMind Ndea

Deterministic optimization aims for a certifiable optimum. Recursive stochastic scaling can become extremely powerful, but its improvement path remains asymptotic.

Appendix

Requirements

Funding for the team and compute needed to test a deterministic approach from theory through industrial deployment.

5-10 Engineers Systems-minded engineers who can work vertically across the abstraction layers of a CUDA-style solver stack: each developing a different component end-to-end.
2 Theorists Algorithm designers to extend the mathematical core: new decomposition theorems, tighter bounds, and the next generation of deterministic methods.
2 Partnerships Operators embedded with chip-design and quant-trading customers to take the solver into production at real industrial workloads.
Compute GPU and cluster capacity to test many variations of the practical algorithm implementations. As we are close to the end, we can just brute force many of this now.

Appendix

Roadmap

Four phases over the next 18 months, each targeting a concrete milestone: a SAT solver, an EDA benchmark, a deterministic model-training prototype, and broader deployment research.

Phase 1

SAT Solver, Summer 2026

Ship the deterministic SAT solver and publish benchmarks against current baselines.
Phase 2

ISPD, Placement & Routing

Compete at ISPD with a deterministic placement engine; target measurable gains on standard benchmarks.
Phase 3

Foundation Model Design

Prototype model-training workflows that use reversed-gradient ideas to reduce search cost and improve auditability.
Phase 4

Deterministic AI Infrastructure

Scale the deterministic approach across selected verticals while expanding the solver library.

Appendix

An Expanding Frontier

This is a new category of AI research, and it is very early. The major labs have poured tens of billions into scaling stochastic methods. Labs focused on Formal Reasoning and Mathematics are only beginning. The space is wide open.

The major labs have mostly focused elsewhere. That leaves room for a specialized team to build a more exact, verifiable, and cost-aware approach to this frontier.

Appendix

Executive Summary

Thesis

Echea builds deterministic SAT solvers and #SAT (model counting) algorithms grounded in algebraic graph theory, spectral graph theory, and algebraic topology, adding more exact, verifiable mathematical structure to heuristic stacks.

Team

Jonathan Belay, Founder & CEO. Harvard CS; founder of Harvard's first AI club; Google Connectomics (pre-training).
Simeon Radev, Co-Founder & CTO. Harvard CS; MIT (AI for NP-Complete protein folding); Etched (NP-Complete chip design).
Henry Bosch, Mathematical Advisor. Harvard CS; Stanford PhD Math+CS; Etched; organizer of the PhD Seminar on Math and Computation.
William Shen, Biopharmaceutical Advisor. Harvard CS; Harvard Med (NP-Complete drug design).
Leslie Valiant, Academic Mentor. Turing Award laureate; T. Jefferson Coolidge Professor of CS and Applied Mathematics, Harvard.

Traction

First research paper, Counting Vertex Covers in Trees (April 2026).
Technical memo, The Year Ahead (March 2026).
Leslie Valiant joining as Academic Mentor.

The Path to a 10× Business (Base Case)

Track record: SAT solvers have become roughly 10,000× faster from the 1980s to today, driven by algorithmic progress, not Moore's Law. The historical curve suggests meaningful algorithmic leverage remains possible.
A 10× improvement on selected industrial workloads is within the historical trend and is the near-term target.
Wrapped in a CUDA-style developer ecosystem (libraries, compilers, benchmarks, tooling), this could address a $10B+ SOM: EDA formal verification, constraint programming, reliability analysis, industrial scheduling and quant-trading order execution.
Beachhead customers: top-5 fabless semiconductor firms (placement & routing) and tier-1 systematic trading firms (order scheduling). Both have clear ROI on single-digit-million contracts.
This alone can be a reasonable, venture-scale business with defensible IP and a mathematical moat.

The Path to a 10,000× Business (Upside Case)

Modern SAT solvers, like modern ML, are dominated by heuristics (CDCL, clause learning, variable ordering, restarts). Heuristics plateau.
#SAT opens a door heuristic-only solvers cannot: algebraic graph theory, spectral graph theory, and algebraic topology offer structural invariants and decompositions that may expose the hidden geometry of combinatorial problems.
If that mathematical toolkit yields exploitable structure on important instance classes, speedups could compound past 10×:
- 100×, broader combinatorial-optimization workloads: logistics, scheduling, hyperparameter and neural-architecture search, feature selection. ~$50B SAM.
- 10,000×+, deterministic solvers could reduce the cost of selected model-training and chip-design workflows now dominated by stochastic or heuristic search. Large AI infrastructure TAM.
The upside case is a real frontier: the major labs have mostly prioritized stochastic scaling. That creates asymmetric room for a focused team if the technical milestones work.

The Ask

5 engineers working vertically across the abstraction layers of a CUDA-style solver stack.
2 theorists designing algorithms (decomposition theorems, bounds, next-generation deterministic methods).
2 partnership leads embedded with chip-design and quant-trading customers.
Compute for running many variations of practical algorithm implementations.

Common Objections (Addressed)

“The SAT solver market is too small.”

The pure SAT-solver licensing market today is roughly $1B. That number is a red herring: it measures revenue generated by today's solvers on today's workloads, a function of solver capability, not of latent demand.

Consider the machine learning analog. In 2012 the commercial neural-network market was a rounding error. Computer vision, NLP, audio, robotics, drug discovery, and recommendation all relied on handcrafted features and shallow classifiers, because deep-network training was intractable at scale. Once GPU training became practical, ML did not merely grow the 2012 market; it expanded into adjacent categories. Those fields collectively became a much larger ML market.

A 10× SAT speedup could trigger a similar dynamic in industries that currently accept heuristic output because more exact methods are too slow: EDA placement and routing, supply-chain planning, quant order scheduling, protein folding and drug design, compiler optimization, constraint-based manufacturing scheduling. The addressable market is broader than today's licensing pool because customers pay for quality, certainty, auditability, and lower search cost.

“P ≠ NP, so this is fundamentally impossible.”

Echea does not claim P = NP as a theorem. That problem is formally open, and nothing we are building depends on resolving it.

But the informal intuition behind this objection, "NP-hard problems must remain intractable on practical instances", is less absolute than it once appeared, and investors should update accordingly.

First, the direct historical evidence. Since 1980, SAT solvers have improved by roughly 10,000× on industrially relevant instance classes. The CDCL revolution alone delivered several orders of magnitude without touching P vs NP. These gains came from exploiting structure in many real instances of NP-hard problems that worst-case complexity theory does not characterize. The trend is still active.

Second, the recent AI signal. The rise of advanced AI systems provides an additional, and in our view under-appreciated, empirical update. Modern large models, which are bounded-size neural networks executing in polynomial forward-pass time, are now demonstrably solving or tightly approximating problems once considered to require exponential search: ad-hoc theorem proving, multi-step planning, combinatorial puzzle solving, code synthesis, and rough formal proofs. This is not a formal proof of P = NP. Worst-case complexity is untouched, and the theoretical question remains open. But it suggests that the practical frontier between "polynomial" and "exponential" is far less strict than classical intuition suggested. Problems previously assumed to require exhaustive reasoning are increasingly being approximated or solved on practical instances by bounded systems.

The rational update. Given recent AI progress, the informal prior that "NP-hard means practically intractable" should be treated with more nuance. Echea is not betting on a proof of P = NP. We are betting that a commercially meaningful fraction of hard practical instances has exploitable structure, and that better structural tools can make those workloads more exact, verifiable, and cheaper to solve.

“Stochastic methods / ML are winning. Why go deterministic?”

Heuristics and stochastic methods dominate today's AI landscape because rigorous alternatives did not exist at scale. That is not an argument against building rigorous alternatives, it is the reason to build them.

Entire categories are difficult to serve with stochastic methods alone:

Chip verification cannot tolerate probabilistic correctness. A fabbed logic bug on a 3nm node costs $100M+ to correct. Chip designers verify with SAT and SMT solvers, and will continue to.
Safety-critical systems (aerospace, medical devices, autonomous vehicles) increasingly require formal proofs rather than statistical guarantees. The FAA does not certify "trained probabilistic landing."
Cryptographic assurance is built on exact computation, not approximation.
Reliability analysis and probabilistic inference in structured domains reduce directly to #SAT. Stochastic sampling gives noisy estimates; #SAT gives exact counts.
AI alignment itself increasingly benefits from formal verification of agent behaviour, policy bounds, and value specifications. As models become more capable, probabilistic behavioural testing becomes less sufficient; the field will need stronger deterministic checks than it currently has.

Stochastic and deterministic methods are complementary, not competitive. Echea is building a deterministic layer for the stack: the part that can make selected workflows more exact, verifiable, and cost-efficient at industrial scale.

“Big labs will just build this themselves.”

They could, but their current incentives and staffing are pointed elsewhere, and the pattern is well documented.

The frontier labs (OpenAI, Anthropic, DeepMind, Meta AI, xAI) have publicly committed enormous capital to scaling stochastic pre-training. Their technical leadership, compute, and roadmaps are structured around improving neural-network training efficiency, not around applying algebraic graph theory and algebraic topology to model counting. Their research output in #SAT and algebraic combinatorics appears limited relative to their work on stochastic scaling.

Even if a frontier lab reallocated a pod to this area tomorrow, they would face a steep staffing problem. The combination of deep combinatorial and #SAT expertise, fluency in algebraic graph theory / spectral methods / algebraic topology, and CUDA-level systems engineering for industrial-scale solver implementation is exceptionally rare. Most people with the first two skills are in academia; most people with the third are at chip companies or high-frequency trading firms. Our team spans all three: Harvard CS theory, MIT research on NP-Complete protein folding, Stanford PhD in Math and CS, Etched chip-design silicon, and Google Connectomics pretraining systems experience. Leslie Valiant as academic advisor attracts downstream research talent into our orbit rather than theirs.

Historically, the large labs have acquired rather than built specialized capability: Google's DeepMind acquisition, Nvidia's Mellanox, Intel's Mobileye. This sector could follow a similar pattern if the technical milestones are achieved.

“This belongs in academia, not a startup.”

Every piece of industrial optimization software shipping today descended from academic research but was built outside the academy. CUDA came from Nvidia, not Stanford. Gurobi, the dominant commercial linear and integer programming solver, with revenue approaching $1B, was commercialized by engineers who left academia for exactly this reason. IBM's CPLEX, FICO's Xpress, Mosek: the same story.

Academic groups publish algorithms; they do not build industrial-scale developer ecosystems, customer-facing toolchains, benchmark suites, or tightly integrated commercial support. Universities do not optimize for integration; their incentive structures favour publication. The value in this space, and the gap, is productizing mathematical breakthroughs at scale. A startup is a practical vehicle, and Echea is structured to operate between academic research and industrial deployment.

“Heuristic solvers are good enough.”

"Good enough" in this sector can still leave large amounts of value on the table. Industries using heuristic optimization often pay a measurable efficiency tax:

In EDA, current heuristic placement and routing tools can leave silicon area, wire length, and power on the table versus stronger optimization. On a flagship TSMC 3nm tape-out costing $300M+, a 3% area improvement is $9M+ per chip family, and a fab ships many families per year.
In quant trading, heuristic order-scheduling can lose basis points of alpha at tier-1 firms, which can be material in absolute terms at a $100B AUM shop. It also often cannot produce the deterministic proof trails that regulators increasingly require.
In logistics and manufacturing scheduling, heuristic operations-research software (the core of the Gurobi/CPLEX market) is priced at low six figures per seat precisely because small percentage improvements in schedule quality translate into meaningful top-line gains.
In drug design, combinatorial search over chemical space is constrained by heuristic methods; enlarging the searchable region by even an order of magnitude materially can increase hit rates in lead discovery.

"Good enough" is often the marketing of current incumbents. Each measurable point of efficiency, cost, or auditability can become a revenue opportunity for better solvers.

“#P-complete problems are decades old and nobody has cracked them. Why would you?”

Historically, many meaningful breakthroughs on #P-complete and adjacent counting problems have come from one mathematical object: the determinant and its surprising algebraic generalizations. The determinant is the canonical example of a polynomial-time-computable function that unexpectedly captures rich combinatorial counting structure, and its generalizations have been responsible for several of the field's celebrated positive results.

Consider the precedent. The matrix-tree theorem (Kirchhoff, 1847) reduces counting spanning trees of a graph, a combinatorial object, to the determinant of the Laplacian matrix, giving a polynomial-time algorithm for a problem that looks exponential on its face. The FKT algorithm (Fisher, Kasteleyn, Temperley) solves counting perfect matchings in planar graphs, which is #P-complete in the general case, in polynomial time, using the Pfaffian (a determinant-like object). Holographic algorithms (Valiant, 2004) generalize this further: families of #P-complete problems can collapse to polynomial time when the problem's structure admits an encoding into matchgates and Pfaffians. Holant problems and matchgate tractability extend the framework still further.

The pattern is consistent: many surprising positive results in #P-complete counting come from determinants, Pfaffians, and their algebraic generalizations. And those generalizations continue to appear. Recent work on spectral characterizations of graph polynomials, algebraic and topological invariants from cohomology applied to constraint satisfaction, and deep connections between #SAT, permanents, and tensor decompositions are actively opening new structural hooks into the #P-complete landscape.

Our team includes Leslie Valiant, the Turing laureate who defined the #P complexity class, proved the #P-completeness of the permanent, and invented holographic algorithms. That is not a coincidence. The intellectual lineage Echea is pursuing is part of the lineage that has produced important breakthroughs in this field, and that lineage is still actively generalizing. The existing body of work on determinants and their extensions is not a dead end; it remains a productive research programme in computational complexity and a natural place to search for the next practical breakthrough.

“Sales cycles in EDA and finance are long.”

Long sales cycles are real. EDA procurement runs 9–18 months; finance procurement runs 6–12 months. The business is designed to manage them.

The founder network is already engaged with tier-1 targets through Etched, prior Harvard and Google relationships, and Leslie Valiant's academic network. Warm introductions exist today.

Pilots are priced asymmetrically against downstream economic value, not against cost: a pilot can be small relative to the value at stake per chip tape-out or trading workflow. Companies selling into conservative sectors often manage long cycles through direct technical engagement, reference customers, and founder-led sales. Echea is structured similarly.

In parallel, the research publication track, first paper shipped, second in progress, is designed to generate pull from adjacent industries. Academic and industrial researchers will bring the technology to their employers as citations and benchmark results accumulate.

Risks & Mitigations

Research risk on the upside case. The 10,000× path depends on breakthroughs in applying algebraic and topological methods to #SAT at scale. Mitigation: the 10× path is not contingent on these breakthroughs, and can generate revenue on its own.
Sales cycle length in EDA and quant trading is long. Mitigation: founder networks already engaged with beachhead targets; pilots can be priced asymmetrically against the headline economic value of even single-digit-percent area or alpha improvements.
Talent density. The intersection of deep SAT expertise and CUDA-level systems engineering is rare. Mitigation: the team's Harvard / MIT / Stanford / Etched / Google network covers both sides, and Leslie Valiant's mentorship materially expands recruiting reach.

Appendix

The Counting Connection

Every SAT problem has a counting twin. SAT asks does a solution exist? #SAT asks how many? Counting subsumes deciding.

Modern SAT solvers are built on heuristics, the same way ML is. #SAT is different: it admits real mathematics, algebraic graph theory, spectral methods, algebraic topology, which heuristics cannot reach. That is the source of the breakthroughs.

Echea

Formal Reasoning for Verifiable AI

Formal Reasoning for Exact AI

One Problem Class. Every Industry.

Shared Optimization Across Industries

SAT Scaling Laws

Recursive Algorithmic Improvement

Beyond Gradient Descent

Limits of Stochastic Training

The Middle Ground

Formal Methods for Model Training

Pre-Training Reversed

Model Training

Chips Perfected

Exact Silicon Optimization

Research & Theory

Research and Technical Work

Counting Vertex Covers

The Year Ahead