Dynamic Formal Systems
The DFS lab is the main research division at Unusupicious. We bridge formal constructions of the world and it's physical substrate. Trying to close the gap between logic and the unsayable.
Main developppement product
A typed prefix-parsing engine for constrained decoding.
The systems is named after Carnap's Der logische Aufbau der Welt. In the same way he tried to built the whole world on a rather small set of construction rules, AUFBAU makes the wager that LLMs guided by a correct-by-construction constraint layer. From a dynamically loaded typed grammar it constructs, token by token, only the continuations that keep a partial syntax tree well-formed and well-typed.
In the technical sense, its a prefix parser for a subset of attribute grammars.
The model interface lives in Proposition 7, where we use an oracle interface in the generation loop that allows us to verify if a token is a valid continuation of the current input. Validity is not only syntactic derivability but also semantic correctess.
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)
?B
AUFBAU grammar file format. Install with pip install aufbau-rs and get started with your own grammar files.
Try it yourself
Two decodes of the same prompt, the same model and the same seed. One runs free; the other may only emit tokens that keep the syntax tree well-formed and well-typed. Load one of our grammars or paste your own, and watch which tokens the engine refuses.
In development
A coding agent whose permissions are a typed declaration, not a prompt.
Every agent that touches a filesystem answers the same question badly:
what is this thing allowed to do? The usual answer is a system prompt
and a wrapper that hopes for the best. GAMMA's answer is a
capability table — read_file,
write_file, list_dir, search,
run — declared in the same typed grammar formalism AUFBAU
already enforces during decoding.
That makes the interesting property fall out for free. The declaration is data, so it can cross a wire that execution cannot: the language a model is constrained by travels to the inference host, while the evaluator, the hosts and the approvals stay on your machine. An agent cannot propose a call it has no capability for, because the tokens spelling it were never admissible in the first place.
GAMMA is the only component in the stack that executes anything, and it is deliberately the smallest. Early development — the language and the capability table are real, the session loop is landing.
// a capability is a typed declaration,
// not a sentence in a prompt
capability read_file :
Path[p] -> Contents
capability run :
Command[c] -> Output
requires approval
// the model is constrained to this
// language while it decodes; the
// evaluator never leaves your box
Γ ⊢ read_file(p) : Contents
--------------------------------
admissible
The declaration crosses the wire. The execution does not.
Publications
Peer-reviewed work from the lab.
To appear · 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.
Accepted and rights-cleared; the DOI resolves once the proceedings appear in the ACM Digital Library. The engine the paper describes is AUFBAU, and the playground above runs it.
Research Focus
Some of our areas of interest.
We are buiding not only an engine but also a genealized theory of completability in context dependent languages. At the frontier between abstract semantics and concrete applications.
Applying computer science techniques to logical reasoning, trying to discover the computational basis of intelligence.
Implementing physical dimensional analysis inside rust's type system with the SLUT crate. Used in simulations and scientific computing.
Making the meta-est theory of typed grammars.
Brzozowski derivatives for prefix validation: decide in one step whether a partial string can still complete to a match.
Developpping a compute substrate for ML that uses parralelizable interaction nets.
State of affairs
Run a grammar against a live model first — then read the code, or talk to the lab.