AxiomCode Graph turns any codebase into a formal-methods-grounded knowledge graph, giving coding agents precise answers to code-related questions. It helps agents make more complete, correct changes while reducing rework, time, and token usage.
We're now building the next layer and will release soon: translating engineering specs and constraints into formal rules on top of the code graph to verify agent-generated changes.
I tried on my TS codebase (80k LoC), it seems similar performance compare with other graph builders (better call depth correctness). Wonder how's others' performance? I will try another larger codebase to see the difference.
Good question, most graphs nowadays rely on Tree-sitter, heuristics, or string-based search for code structure analysis. What we do here is using formal methods through data-log rules instead of lean. This fundamental different approach achieve 94.9% accuracy as result on Defects4J Benchmark, compare with Graphify 48.7%
Couldn't agree more, and we (not just us but the whole industry) are just getting started. However, what we see there is lean is not the only path to do it, and that why we are trying to do with a different scalable formal rules approach.
AxiomCode Graph turns any codebase into a formal-methods-grounded knowledge graph, giving coding agents precise answers to code-related questions. It helps agents make more complete, correct changes while reducing rework, time, and token usage.
We're now building the next layer and will release soon: translating engineering specs and constraints into formal rules on top of the code graph to verify agent-generated changes.
I tried on my TS codebase (80k LoC), it seems similar performance compare with other graph builders (better call depth correctness). Wonder how's others' performance? I will try another larger codebase to see the difference.
How are you using formal methods? How is it different from other similar graphs for agents?
Good question, most graphs nowadays rely on Tree-sitter, heuristics, or string-based search for code structure analysis. What we do here is using formal methods through data-log rules instead of lean. This fundamental different approach achieve 94.9% accuracy as result on Defects4J Benchmark, compare with Graphify 48.7%
Formal verification code graphs are the need of the hour
Couldn't agree more, and we (not just us but the whole industry) are just getting started. However, what we see there is lean is not the only path to do it, and that why we are trying to do with a different scalable formal rules approach.
I'm going to check it out!
Awesome, try it with your coding agents! Let us know if there is any question or feedbacks!