SharpLogic: Formalizing Bug Detection for LangGraph Routing Graphs with k-CNF

The reliability of multi-agent workflows has always been a weak spot for frameworks like LangGraph and CrewAI. When routing and retry logic intertwine, evals often only tell you "it's wrong" but can't explain "which path will deadlock." Recently, an open-source project called SharpLogic attempts to bring this problem back onto the track of formal verification: it maps agent routing and retry graphs into k-CNF, then uses a Rust kernel to count deadlocks and failing paths (the #F count), letting developers run gate checks on the graph before release.

From "Run It and See" to "Compute Exactly How Many Bad Paths Exist"

The core idea of SharpLogic is converting graphs into logical formulas. A LangGraph-style multi-agent flow is essentially a directed graph: nodes are agents or tools, and edges are routing conditions and retry policies. The project encodes this graph as k-CNF (conjunctive normal form), turning "does a deadlock path exist" and "how many failing paths are there" into computable problems. In the Reddit post, the author revealed that the demo case contains 20 variables, corresponding to a 2^20 state space, and the offline check takes only microseconds.

According to the post, SharpLogic provides a Python-side AgentGuard hook and a command-line tool, allowing developers to run a formal health check on the graph in CI or before release. It doesn't aim to prove grand propositions like "we've solved ETH"; instead, it positions itself as a local engineering tool, open-sourced under the MIT license, hosted on GitHub, and accompanied by an online demo (the demo uses ETH-2026 as sample code).

k-CNF and #F Counting

k-CNF (k-conjunctive normal form) is a standard form of propositional logic formulas: a conjunction (AND) of several clauses, each clause being a disjunction (OR) of at most k literals (variables or their negations). For example, (x₁∨¬x₂)∧(x₃∨x₄) is a 2-CNF. Any Boolean combinational logic can be transformed into an equisatisfiable CNF by introducing auxiliary variables, so it is often used as an intermediate representation in hardware and software formal verification. Once an agent routing graph is encoded as k-CNF, "does a deadlock path exist" becomes equivalent to asking whether the formula is satisfiable (SAT).

#F counting goes further: it counts the number of assignments that make the formula true, a counting problem in the #P complexity class (a generalization of #SAT). In SharpLogic's context, each assignment corresponds to one combination of conditions in the graph, and the count directly reflects "how many paths will fail" or "how many combinations lead to deadlock," upgrading a binary Boolean judgment into a quantification of the failure surface's scale.

Model Checking and Property-Based Testing

Model checking is an automated formal verification technique: first build a finite-state model of the system, then exhaustively or symbolically search its state space using algorithms to check whether given temporal logic properties hold (e.g., "will never enter a deadlock state"). It either provides a proof that the property holds or returns a concrete counterexample path. Property-based testing approaches from the other side: it uses generators to randomly produce large numbers of inputs, checks whether the code always satisfies some invariant, and automatically shrinks to a minimal counterexample upon failure.

SharpLogic sits between the two—it doesn't execute agents but performs symbolic analysis on the graph structure, thus combining the exhaustiveness of model checking with the lightweight nature of property-based testing. Understanding this spectrum helps determine its applicable boundaries: routing/retry logic with enumerable state spaces is suitable for formal methods, while agent behavior depending on open text or external services still requires evals and property-based testing as a fallback.

Formal Bug Detection and Evals: Complementary, Not Replacement

The question posed in the post is straightforward: can formally defining handoffs this way catch bugs that evals miss? The author's stance is pragmatic—evals excel at measuring output quality and task success rates but are insensitive to structural defects like "will a certain retry path loop infinitely" or "does a certain combination of conditions lead to no solution." Formal checking fills exactly this gap: it doesn't run models, only analyzes graph structure, so it's fast, offline, and deterministic.

But this doesn't mean it's "smarter." What k-CNF encoding and #F counting can cover is the finite state space of routing and retry logic, provided the graph is modeled correctly. If agent behavior itself depends on non-enumerable external states (such as open text returned by tools), the formal model can only handle it abstractly, potentially producing false positives or false negatives. The author also acknowledges that turning theory into a practical algorithm still requires research, and OpenAI's preprint serves only as background reference.

Community Feedback Focus: Modeling Costs and Practical Boundaries

In the post, the author solicits experience from builders, particularly wanting to understand the effectiveness of similar approaches like model checking and property tests in real projects. Judging from the framing, SharpLogic's potential value lies in shifting "post-hoc debugging" forward to "pre-release gating," but the adoption barrier is also clear: developers must first organize their routing graphs into an encodable form, which itself involves effort. For early-stage projects with frequently changing graph structures, the cost of maintaining formal models may outweigh the benefits; for long flows with stable routing logic but complex retry policies, the benefits will be more obvious.

Another noteworthy point is the significance of #F counting. Compared to a Boolean "is there a deadlock," path counting provides the scale of the failure surface, helping judge problem severity. This is especially practical in multi-agent systems—a retry deadlock triggered only under specific condition combinations is often extremely hard to reproduce in evals but may be hit by occasional traffic in production.

Summary

SharpLogic represents a pragmatic type of attempt: rather than pursuing general theorem proving, it performs localized formal checks targeting the specific structure of agent graphs. Whether it can become a standard tool in the LangGraph ecosystem depends on two things—whether the modeling experience is lightweight enough, and whether formal checking can reliably catch real defects in evals' blind spots. The author's open-source stance and online demo lower the cost of experimentation; for teams building multi-agent workflows, it's worth running a small graph through it first to see.

One-line Summary

SharpLogic encodes multi-agent routing graphs as k-CNF and uses #F counting to formally detect deadlocks and failing paths before release.

Paragraph Summary

SharpLogic is an MIT-licensed open-source project that aims to add formal verification capabilities to multi-agent frameworks like LangGraph and CrewAI. It encodes the directed graph formed by agents' routing conditions and retry policies as k-CNF, then uses a Rust kernel to count deadlocks and failing paths (#F counting), upgrading "does a bad path exist" to "how many bad paths are there." The project provides a Python-side AgentGuard hook and CLI for gate checks in CI or before release; the demo case has 20 variables and a 2^20 state space, with offline checks taking microseconds. The author emphasizes that formal checking and evals are complementary: the former catches structural defects, the latter measures output quality. The adoption barrier is the need to first organize graphs into an encodable form, making it suitable for long flows with stable routing and complex retries.