Research
Formally verified AI
A decoder enforcing semantic constraints on language models.
published
Agents forget the shape of a tool call, mistake the type of an in-context variable, or touch data they may not. AUFBAU rules that out while the model decodes.
Token by token, it builds continuations that keep a partial syntax tree well-formed and well-typed. The constraints are attributes you define on a context-free surface. They range from type constraints to relational rules between objects.
You give the model hard rules, and it cannot break them.
The safe-pruning proof is a paper proof of the rejection rules, not a mechanised proof of the code. Completion holds only for grammars that meet the paper's conditions. Nothing here says the output is true.
Variable(var) ::= Identifier[x]
BaseType ::= Identifier | '(' Type ')'
AtomicType ::= BaseType | '(' Type ')'
FunctionType ::= AtomicType '->' Type
Type ::= AtomicType | FunctionType
Lambda(lambda) ::= 'λ' Identifier[a] ':' Type[τ] '.' Expression[e]
AtomicExpression ::= Variable | '(' Expression ')' | Lambda
Application(app) ::= Expression[l] AtomicExpression[r]
Expression ::= AtomicExpression | Application
x ∈ Γ
----------- (var)
Γ(x)
Γ[a:τ] ⊢ e : ?B
--------------------------- (lambda)
τ → ?B
Γ ⊢ l : ?A → ?B, Γ ⊢ r : ?A
--------------------------------- (app)
?BRevolutionary text corpus
A corpus of revolutionary press, and a training design that keeps an international base apart from a situated post-training.
work in progress
KARL assembles a corpus of revolutionary press and archives to train a writing model on a base of Marxist classics in several languages. The unit is the article or the whole chapter, never an arbitrary chunk. The political line is set in post-training, not in the pretraining data.
Supervised pairs are built backwards. The response targets are published texts, and only the question that elicits each text is generated.
Hugging Face · dfslab · Project notes
The code is private. There are no public checkpoints or datasets, and the project notes are dated September 2026.
Critical AI & Information research
A framework that queries diffusion models in their own latent space.
experimental
SLOP queries a diffusion model directly in its latent space. It captures latents, noise predictions and embeddings while the model generates, and measures how the model renders identity, geography and politics. It also locates where those biases sit as geometry in that space.
Inference runs on restricted HPC. The client tunnels a binary protocol over SSH to a GPU node with no open ports. A distilled-checkpoint registry keeps a sweep affordable.
SLOP produced the visualisations of the Holy Slop installation, shown in The World Through AI at SCHIRN and in Hidden Layers at UC Berkeley.
Published · October 2026
In Proceedings of the 2nd ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL '26), October 4–9, 2026, Oakland, CA, USA, pages 13–23.
Exhibition · 2026
Using our SLOP framework we produced visualizations used in a piece of the World Through AI exhibition at SCHIRN Kunsthalle in Frankfurt, later shown in Hidden Layers at UC Berkeley. The piece displayed visualizations of differential diffusion fields between neutral embeddings and a Palestinian identity prompt. We identified racist and orientalist representations that matched to attracting areas of the diffusion field.