Research

Aleph

A functional programming language I designed and implemented — grammar, type checker, code generation and standard library. Aleph compiles to native code and calls directly into C, assembly, LLVM IR and WebAssembly through a native foreign-function interface, so a program can reach a POSIX syscall without a runtime standing in the way.

The SDK covers errors and recovery policy, resource disposal with full propagation, a JSON algebraic data type with per-type codecs, equality dictionaries, a filesystem module that discriminates real error cases through access(2), and a test framework with TAP output and property testing. Sixty-one tests across eight suites.

• Compiler design
• Type systems
• FFI
• LLVM
• WebAssembly

• Syntax reference →

Genesis

Eleven packages for building languages: a monadic parser-combinator library with LINQ support, an EBNF grammar compiler that emits executable combinators, an ASDL schema parser that generates C# AST types, a forward-chaining rule language, a TLA+ checker with LTL evaluation, and a symbolic algebra system that differentiates, integrates, expands and solves.

On top of that sits an application factory. A domain description becomes a formal specification, the specification is model-checked before anything is built, and the build follows from the specification rather than from a prompt. The method borrows TOGAF for what exists, Gilb’s Planguage for what must hold, and reactive DDD for what to build — with one rule doing the real work: the language model acquires content, rules admit it, and what is missing is derived rather than guessed.

The reasoning layer, Thinker, is where the neural and the symbolic meet: pluggable LLM providers and retrieval-augmented generation acquire knowledge, a deterministic grammar formalises it, a forward-chaining engine proves over it, and a symbolic reinforcement learner improves what is believed over time. The LLM never answers — only proofs do.

• C#
• .NET 10
• Parser combinators
• EBNF
• ASDL
• TLA+
• Symbolic algebra
• LLM integration
• RAG
• Reinforcement learning

• Documentation →
• NuGet →
• All Genesis packages →

MLambda.Actors

A reactive actor framework for .NET: a root/system/user/temp guardian hierarchy with parent–child supervision, one-for-one and all-for-one strategies, runtime behaviour switching, message stashing and replay, death-watch, and full lifecycle hooks. Every response is an IObservable<T>.

Beyond the single process it clusters — gossip-based membership, mTLS between nodes, and gRPC transport — and the same actor code runs standalone, hybrid or clustered depending on configuration alone.

• C#
• .NET
• System.Reactive
• gRPC
• Kubernetes
• mTLS

• Documentation →
• NuGet →

MLambda.Data

A distributed database in which every component is an actor — storage, indexes, filesystem, query planning and authorisation alike. There is no shared mutable state and there are no mutexes in the data path; correctness comes from message ordering rather than from locks.

The storage engine is log-structured: write-ahead log with CRC32 integrity, an in-memory sorted memtable, immutable SSTables, and background compaction under a throttle. Indexes cover sorted range queries, O(1) point lookups, probabilistic existence checks and full-text search. The cluster layer places data on a consistent hash ring and replicates metadata through CRDT gossip. The consistency model is specified in TLA+ and model-checked, not merely described in prose.

• C#
• .NET 10
• LSM storage
• CRDT
• Consistent hashing
• TLA+

• Documentation →

Hilbert — Incremental Strange Loop Transformer

Neuro-symbolic AI built on a claim worth testing: a transformer’s attention layer is mathematically an adaptive filter with feedback, which means it can be made to learn from each input without retraining.

Five levels, each carrying a different logic — first-order, relational with graph attention, modal with a multi-world attention matrix, temporal with LTL and dual causal/bidirectional attention, and sortal with ontology-biased attention. They are connected by fast weights and episodic memory, and by a strange loop after Hofstadter that feeds the top level’s error signal back down to refine the lower four at inference time. A genetic layer maintains populations of fast-weight configurations, so evolutionary exploration and gradient descent run against each other.

This is active research. There is no public release yet.

• Python
• PyTorch
• Transformers
• Graph attention networks
• Fast weights
• Meta-learning (MAML)
• Modal logic
• Temporal logic

MLambda.UI

A UI framework that never calls a render method. Components describe an atom tree; rendering backends walk it and paint. The same view code runs on desktop through ImGui, in the browser through Blazor WebAssembly, and natively through Avalonia, unchanged.

Styling is algebraic — Morphe = Geometry × Color × Font — so styles compose like expressions rather than cascading and overriding. State is Observable<T> and Computed<T> on Rx.NET, and the Control → ViewModel → View → Design separation is enforced by the type system rather than by convention.

• C#
• Rx.NET
• ImGui
• Blazor WebAssembly
• Avalonia

• Documentation →

MLambda.OS

A Minix 3-inspired microkernel for x86-64, written to understand operating systems by building one: CPU feature detection, the GDT and IDT, paging, protection rings and the syscall boundary, then processes, IPC, memory management, a filesystem and I/O. Specified before it is implemented, one subsystem at a time.

• Rust
• C
• x86-64
• Assembly

• Documentation →

Automation architectures — the BEAM method

The pipeline that produces the systems above, and the reason they get built at the pace they do. A business domain is decomposed into a knowledge graph, turned into an actor topology with an explicit supervision hierarchy, refined into a purified Z specification, and model-checked in TLA+ — and only then implemented, with the tests derived from the model rather than invented afterwards.

Four claims hold it together: a missing requirement is an unfulfilled obligation to be deduced rather than guessed; a waiver is a belief and closes nothing until a person grounds it; the aggregation is derivable, because the connected components of the invariant graph are the aggregates; and design estimates while verification measures — the difference between them is what the method learns.

• Z notation
• TLA+
• Reqnroll
• Docker
• Kubernetes

• The method →