Inspiration
Rules control an enormous part of our lives: who qualifies for opportunities, when deadlines apply, what software is allowed to do, and what happens when exceptions collide. But most rules are tested using only a handful of examples.
We became interested in a different question:
What if we could mathematically test what might happen before it actually happens?
Archimedy was inspired by the idea of treating rules the same way engineers treat critical systems: instead of waiting for a rare edge case to cause a failure, search for that edge case ahead of time.
The challenge is that even simple systems can have millions or billions of possible combinations. Testing them individually would be impossible. That led us to build Archimedy around symbolic reasoning rather than brute-force simulation.
What it does
Archimedy turns rules into a mathematical model and searches the space of possible situations for failures.
It can look for:
- contradictions between rules
- ambiguous interpretations
- uncovered cases
- impossible combinations of requirements
- boundary and deadline problems
- exception conflicts
- eligibility cliffs
- unexpected differences in outcomes
Instead of checking every possible case individually, Archimedy represents large groups of equivalent cases symbolically.
For example, if a system contains variables with (n_1,n_2,\ldots,n_k) possible values, naive testing may require:
[ N=\prod_{i=1}^{k} n_i ]
individual cases.
That number can quickly reach millions or billions.
Archimedy attempts to reason over those possibilities using a much smaller symbolic representation and then produces a concrete witness when it finds a problem: an exact combination of inputs that reproduces the failure.
The most important design decision is that Archimedy separates proof from estimation. If exact analysis succeeds, the result can be reported as proven within the encoded model. If the symbolic problem becomes too complex, Archimedy stops claiming proof and switches to clearly labeled statistical analysis instead.
How we built it
The core of Archimedy is deterministic rather than generative.
Rules are converted into structured variables, predicates, constraints, and outcomes. The analysis engine then operates on this representation using symbolic-state exploration and constraint reasoning.
We also added feasibility constraints so Archimedy does not waste time analyzing impossible situations.
For example, the raw encoded space in one of our tests contained:
[ 10,790,021,580 ]
possible profiles.
After applying feasibility rules, the true valid population was reduced to:
[ 4,565,009,130 ]
profiles.
Archimedy could then compare different interpretations of the rules without explicitly iterating through all 4.5 billion valid profiles.
AI is used primarily as an interface layer to help translate human-readable rules into structured information. The important verification work remains deterministic so the system is not relying on an LLM simply saying that a contradiction exists.
Challenges we ran into
One of our biggest challenges was realizing that simply having an enormous search space does not make an analysis meaningful.
Our first approaches could accidentally include logically impossible profiles. That meant the system could find technically valid mathematical counterexamples that could never exist in reality.
We fixed this by introducing explicit feasibility constraints before counting or analyzing states.
Another major problem was symbolic complexity. Decision diagrams and similar representations can compress billions of possibilities extremely well for some problems, but certain rule structures can cause the symbolic representation itself to grow dramatically.
Instead of hiding that limitation, we added a complexity boundary. Exact analysis stops when the symbolic problem exceeds that boundary, and Archimedy can fall back to a statistical estimate with confidence information.
That prevents the system from presenting an approximation as mathematical proof.
Accomplishments that we're proud of
We tested the mathematical core extensively.
- 5,000 randomized verification tests passed against independent brute-force enumeration.
- One policy model represented 10,790,021,580 encoded profiles.
- Feasibility constraints reduced that to 4,565,009,130 valid profiles.
- Two interpretations of the same rules disagreed on exactly 112,050,000 profiles.
- Archimedy represented the relevant analysis using only 480 symbolic states and produced a reproducible witness.
- In another benchmark involving 300 rules, the system analyzed all
[ \binom{300}{2}=44,850 ]
rule pairs with a median runtime of approximately 0.235 seconds.
We are especially proud that the system does not treat "AI confidence" as proof. A result is only presented as exact when the deterministic analysis can justify it.
What we learned
The biggest thing we learned is that scaling analysis is not just about making code faster.
The more important question is:
Can we change the representation of the problem so we never need to perform billions of individual operations in the first place?
That led us from brute-force enumeration toward symbolic representations.
We also learned how important it is to separate three different ideas:
- what is logically possible,
- what the rules actually say,
- what a testing system can prove.
A system can produce very convincing results while still being mathematically wrong if those distinctions are ignored.
Building Archimedy forced us to think carefully about verification, combinatorics, constraint systems, complexity limits, counterexamples, and the difference between exact and probabilistic conclusions.
What's next for Archimedy
Our goal is to expand Archimedy from a rule-analysis engine into a general system for testing consequences before deployment.
We want users to be able to provide policies, specifications, contracts, workflows, regulations, or software requirements and ask:
"What can go wrong?"
Future versions could automatically identify the smallest rule change that removes a contradiction, compare multiple versions of a policy, analyze software behavior against written requirements, and continuously test systems as their rules change.
The long-term vision is simple:
Before a rule affects millions of people or a system reaches millions of users, Archimedy should be able to explore what that rule or system could do first.
Log in or sign up for Devpost to join the conversation.