Chiasmus is a neurosymbolic verification engine packaged as a TypeScript library and Model Context Protocol (MCP) server. It bridges LLMs with formal solvers — Z3 (SMT) and SWI-Prolog (WASM) — by translating natural-language problems into template-based formal specifications that are verified with mathematical certainty. It also performs static code analysis: tree-sitter-based extraction of call graphs for TypeScript/JavaScript, Python, Go, Rust, Clojure, Scheme, Racket, and Common Lisp, followed by 16 analyses (reachability, dead code, impact, cycles, layer violations, community detection, hubs, bridges, diffs). Architecturally, the repo is a modular ESM library with an MCP server entry point (src/mcp-server.ts) exposing 11 tools over stdio (chiasmus_graph, chiasmus_map, chiasmus_formalize, chiasmus_verify, chiasmus_search, chiasmus_review, chiasmus_learn, etc.). Core subsystems: graph extraction with per-file content-hash caching and snapshot diffing; a formalization engine that selects from 8 built-in skill templates via BM25/embedding retrieval and runs an LLM-driven correction loop against the solvers; a SQLite-backed skill library that learns new templates from verified solutions; and pluggable LLM adapters (Anthropic, OpenAI-compatible, Azure, local via node-llama-cpp). Data flows: source files are parsed by tree-sitter into a CodeGraph, which can be emitted as Prolog facts for symbolic queries or analyzed natively with O(V+E) algorithms (Tarjan SCC, BFS). For verification, a problem statement is embedded, matched to a template, slot-filled by an LLM, linted, and iteratively corrected until the Z3/Prolog solver confirms the property or finds a counterexample. The benchmark suite compares Chiasmus against traditional implementations across RBAC, dependency resolution, taint analysis, workflow validation, and validation consistency. Maintenance is active (v0.1.28, CI on Node 22/24, 70+ test files covering graph extraction, solvers, MCP tools, search, and skills). The codebase is well-engineered with several genuinely reusable components — native graph algorithms, an LRU extraction cache, a BM25 index, and a tsconfig alias resolver — though some coupling exists between the extractor and the TypeScript type environment, and the vendored WASM grammars require periodic upstream syncs.
Scallop is a differentiable probabilistic Datalog engine implemented in Rust with Python bindings (scallopy). It compiles Scallop programs (a Datalog variant with provenance annotations) through a three-stage compiler (front AST → back normalized Datalog → RAM relational algebra) to a runtime that executes with configurable provenance semirings (unit, boolean, tropical, probabilistic, differentiable, etc.). The system supports neuro-symbolic AI by integrating with PyTorch for gradient-based learning, and provides plugins for LLMs (GPT, Gemini) and vision models (CLIP, OWL-ViT, SAM). The architecture is a monolithic Rust library (core) with multiple sub-crates for CLI tools (scli, sclc, sclrepl), Python bindings via PyO3, and a plugin system for extending with foreign functions, predicates, and attributes. Key data flows: user-provided Scallop source or facts are parsed, analyzed (type inference, boundness), transformed, and compiled into a relational algebra plan that is executed with provenance-aware dataflow operators, producing output collections. The codebase is well-structured with clear separation between compiler, runtime, and provenance layers, and includes several reusable components such as copy-on-write containers, galloping search, dual numbers for AD, batch streaming abstractions, and a self-contained SDD library for weighted model counting. While the code demonstrates strong engineering and research-grade sophistication, there is some code duplication across provenance variants and experimental/legacy directories that lower the overall quality score. The repository is actively maintained with recent commits, CI workflows, and a growing plugin ecosystem.