A Fact-Producing Compiler

Series note: this article is part of the Concrete series and responds to Dmitri Sotnikov’s Giving LLMs a Formal Reasoning Engine for Code Analysis. Related: When the Compiler Is the Oracle and Why Concrete Exists.

When an AI agent explores a codebase, it usually greps for names, reads a few matches, searches for callers, reads those, and tries to piece together a mental model of the program from text fragments. This works about as well as you would expect. The agent is asking structural questions about a program, things like “can user input reach this SQL query?” or “what changes if I touch this function?”, but the only tool it has is text search.

Yesterday I read Dmitri Sotnikov’s article about giving LLMs a symbolic reasoning engine for code analysis. His tool, Chiasmus, parses source code with tree-sitter (a syntax parser), turns definitions and calls into logic facts, and lets an LLM run graph queries instead of grepping through files. That is a much better interface: the agent asks a structural question and gets a structural answer.

Reading the post gave me a better phrase for part of what we are building with Concrete: a fact-producing compiler.

Concrete is the systems programming language we are building for programs that need auditability. The point is not only to compile code into an executable, but also to compile code into checked statements about what that executable can do.

#From syntax to semantics

Chiasmus works by recovering structure from source code after the fact: it parses files, extracts which functions exist and what calls what, and turns that into queryable facts. For existing languages that were never designed to expose this information, that is the practical approach.

Concrete can go further because the compiler already knows more than syntax. Tree-sitter can see that foo calls bar, but the Concrete compiler also knows that bar requires Network authority, that foo carries that authority in its signature, and that the call chain crosses a trusted FFI boundary.

By authority I mean what code is allowed to do: allocate memory, read files, touch the network, call unsafe code, cross into foreign code. In Concrete, those permissions are part of the program the compiler checks. They are not comments and they are not recovered later by a scanner.

Today the compiler exposes this as a human report. An authority report on our JSON parser shows where allocation comes from:

capability Alloc (13 functions):
  pub store  <- store -> vec_push
      parse_string  <- parse_string -> store
  pub parse_value  <- parse_value -> parse_string
      parse_array  <- parse_array -> vec_push

Read one line like this: parse_value needs allocation because it calls parse_string, which eventually stores bytes in a vector.

The compiler tracks capabilities (File, Network, Alloc, etc.) in function signatures, enforces them transitively, and can report the path that explains why a function needs some authority. It also tracks execution shape: direct recursion, mutual call cycles, and loop boundedness. The predictable profile is stricter: it rejects unbounded loops, recursion, allocation, FFI, and blocking.

For proofs, the same rule applies. A report can say whether a claim was merely reported by the compiler, enforced by a compiler check, proved in Lean (a proof assistant), or accepted because of a trusted assumption. Proof evidence is attached to the function name and body fingerprint, so changed code cannot silently keep stale proofs.

All of this is available today as human-readable reports. The next step is to make these facts machine-queryable so that agents, CI, and review tools can use them directly.

#What querying looks like

Consider a routine scenario. A reviewer opens a PR that bumps a dependency. The new version reads environment variables three layers deep in a helper. In Rust, nothing in the function signatures changes and the reviewer has to diff the dependency source or hope the changelog mentions it. In Concrete, the function that calls into that dependency must have declared Env authority or the build breaks.

I want the same kind of interface for every compiler fact, not just capabilities. Here is what that could look like. An agent or tool asks a question, and the compiler returns a checked answer:

“Can the packet parser core touch the network?”

{
  "reachable": false,
  "from": "main.decode_header",
  "to_capability": "Network",
  "evidence": "compiler-checked call graph and capability facts"
}

“Why is main not predictable?”

{
  "violations": [
    {
      "gate": "no_blocking",
      "capability": "File",
      "path": ["main.main", "std.fs.read_to_string"]
    }
  ]
}

“Which dependency widened authority since yesterday?” Because the compiler tracks the authority chain for every function, it can return the path.

The model can explain the result. The compiler should supply it.

#What we have and what comes next

Working now: authority, allocation, unsafe, effects, and evidence reports. Recursion, call-cycle, and loop-boundedness classification. Predictable-profile checking. Proof identity with body fingerprints, stale-proof reporting, and selected Lean proof evidence.

Next: source locations and Elm-like diagnostics for report failures. Machine-readable fact output and a query CLI. Semantic diff, trust drift, and module policy gates. Then MCP, or an equivalent agent interface, over the same facts.

The fact artifact comes first. Query CLI, MCP, CI checks, review tools, and agent integration should all read the same checked facts.

#The compiler should say what is true

A compiler should say what is true about the program, not only “type check passed.” What can this function touch? Is it recursive? Are its loops bounded? Does it cross FFI? Is the proof current? Which path explains the authority?

Those are program facts. Concrete produces some, enforces some, and proves some. Now we are making them queryable.