# Magmide is a dormant research project for bringing proof assistants to systems programmers

> Magmide is an experiment in a dependently typed proof language aimed at bare metal systems code, built around a split Logic and Host architecture with a full separation logic at its core. The README states plainly that the repository is dormant, early and rough, and the tree is mostly notes, speculative writing and exploratory theorem proving rather than a usable tool.

**magmide/magmide** — A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

- Repository: https://github.com/magmide/magmide
- Stars: 839 · Forks: 15
- Language: Rocq Prover
- License: not declared
- Published: 2026-10-20 · Updated: 2026-10-20 · Language: en
- Canonical page: https://hysenlabs.com/projects/magmide-magmide

## The README opens by telling you not to use it yet

The first line of the README is a construction emoji and a sentence: Magmide is dormant for now as I rethink what it could or should be.

The next paragraph is equally direct. The repository is still very early and rough, it is mostly just notes, speculative writing and exploratory theorem proving, and most of the files are mad scribblings that the author has not refined enough to actually stand by.

That framing is the single most important fact about the project, and it should shape how you read everything else. There is no compiler here to build, no language to install and no documentation to follow. The primary language listed for the repository is the Rocq Prover, which is the proof language the work is written in, and the licence is not stated, which means there is no permission to reuse, modify or redistribute what is in the tree.

The last push to the repository was on 2026-05-14, and the project publishes no releases. So the correct way to approach Magmide is as a research notebook with an unusually thoughtful README, and the correct way to evaluate it is by reading the reasoning rather than by running anything.

The README does point at a video presentation that covers the core ideas and the design goals, for readers who would rather listen than read.

## The goal: make formal verification practical for working engineers

The stated goal of the project is to create a programming language capable of making formal verification and provably correct software practical and mainstream, with a language and education and tooling ecosystem strong enough to create verified software for any system or environment.

The argument for that goal starts from the damage software causes. The README cites a report on the cost of software errors, statistics on hacking, and a cost estimate for software bugs, and argues that Tony Hoare's estimate of the cost of a single null error was too conservative once you include more than null errors.

The technical premise is that proof assistant languages such as Coq let you define logical assertions as code and write proofs of those assertions that can be checked automatically for consistency and correctness. The problem, in the author's reading, is that such systems were suited only to niche academic applications until the fairly recent invention of separation logic, a paradigm for making logical assertions about mutable and destructible state.

The point of the argument is not that verification is impossible in practice but that it happens in the wrong place. The existing academic systems verify models of programs rather than the programs themselves, and the people who write them are not the people who ship software.

## Separation logic, and the argument from Rust

The README's central technical reference is separation logic, and the argument runs through Rust.

Separation logic is not a tool but a paradigm for making assertions about mutable and destructible state, and the Rust ownership system was directly inspired by it, which the author takes as evidence that the paradigm can unlock large productivity gains. Where functional languages respond to the same problem by outlawing mutation and side effects, separation logic makes it possible to verify practical imperative code instead.

The claim about Rust is a qualified one. Rust exposes only a simplified subset of separation logic rather than the full power of the paradigm. The Iris separation logic was created by a team of academics to fully verify the correctness of the Rust type system and several core implementations that use unsafe, and the author argues that Iris is uniquely capable of verifying the complex, concurrent, arbitrarily flexible assertions that practical Rust code could imply.

Then comes the turn. The README observes that as is common with academic projects, Iris is only being used to write papers rather than real software systems, that existing uses of Iris perform the proofs on the side by analysing manual transcriptions of source code as Coq notation rather than reading the original source directly, and that the resulting papers are still academic papers that essentially no working engineers have heard of.

That is the diagnosis the whole project is built against, and it is a specific one: the proofs do not attach to the code that runs.

## The split Logic and Host architecture

To reach the goal, the author has chosen an architecture called the split Logic and Host architecture, which separates the two domains of software thinking into two languages.

Logic is the dependently typed lambda calculus of constructions, and it is where imaginary types are defined and proofs are conducted. Host is the imperative language that actually runs on real machines.

The two must have a symbiotic relationship. Logic is used to define and make assertions about Host, and Host computationally represents and implements both Logic and Host itself. That second half is the striking requirement, because it means the host language is responsible for running the logic that verifies it, which is a self reference the design has to close somehow.

The comparison the author reaches for is that Magmide is intended to be to Coq what Rust has been to C. The argument is that the existing proof languages are not designed for working engineers to build real imperative programs, that none of them place a full separation logic at the heart of their design, and that instead they are overly dogmatic about the pure functional paradigm. The README also names research debt, the accumulation of obtuse and unapproachable conventions, as the thing that has to be unwound.

The final paragraph of the visible README turns to what would follow if verification were mainstream, asking which ambitious projects have been conceived but not pursued because getting them working would be too difficult, and listing secure operating systems, trustless networks and electronic voting as the kind of thing that machine checkable proofs in many more hands could make possible.

## What is actually in the tree

The directory listing explains the nature of the repository better than any summary could.

There is a theory/ directory, which is where the proof work lives, and the justfile's build and fullbuild targets work inside it, running make and generating a Coq makefile with coq_makefile from a _CoqProject file. There is an src/ directory, and the Cargo.toml defines a package named magmide at version 0.1.0 with the Rust edition 2021, whose only declared dependency is nom, a parser combinator library.

The Cargo.toml also shows what has not happened yet. The library section with a staticlib and cdylib crate type is commented out, as is the build script with its LLVM linking flags. The project is not yet a library that other code links against.

The rest of the tree is documentation and history. There are notes.md and a notes/ directory, posts/ for writing, mg_examples/ for examples, iris-notes.md for the separation logic research, old/ for discarded work, and a README.future.md that sits next to the current README.

The primary language being a proof assistant rather than a systems language is the clearest summary of where the effort is going. The Rust side exists to host the logic, and the logic side is where the work is.

## Two build systems, tied together with just

The justfile is short and shows the two halves of the project side by side.

The test target runs the Rust tests and the Coq tests.

```bash
test:
	cargo test
	dune runtest
```

The build target only touches the theory directory.

```bash
build:
	#!/usr/bin/env bash
	pushd theory
	make
	popd
```

And the fullbuild target regenerates the Coq makefile before compiling.

```bash
fullbuild:
	#!/usr/bin/env bash
	pushd theory
	coq_makefile -f _CoqProject *.v -o Makefile
	make clean
	make
	popd
```

The lab target is a scratchpad. It runs the Rust program with cargo run, then runs lli-13 on a compiled lab.bc, which points at a specific LLVM 13 toolchain that the commented out build section also references. The clean target removes the Coq build products, the glob, vo, vok and vos files and the aux and lia cache files, and the Makefile itself.

The presence of dune runtest alongside coq_makefile suggests the theory side has been through a move from plain Coq makefiles to dune, and that both are still supported. That is the kind of detail that is normal in a research repository and would be tidied in a release.

## Why this is a design document, not a dependency

It is worth being explicit about what Magmide is not, because the name and the topic list can suggest otherwise.

There is no language to install, no package on a registry, and no release. The version in the Cargo manifest is 0.1.0 and the crates.io entry the manifest implies is not published. There is no stated licence, which for a repository of ideas and proofs means nobody else may legally build on it without permission.

What there is, is a set of notes that argue a particular thesis. The thesis is that proof assistants could be mainstream if they were designed for imperative systems programming, if they exposed a full separation logic rather than a simplified subset, and if they attached their proofs to the source code instead of to a transcription of it. The split Logic and Host architecture is the proposed answer, and the ecosystem around a language, the education and the tooling, is treated as part of the problem rather than as a separate concern.

For a reader working on verification tooling, that is a well argued position with a concrete design attached, and it is cheap to read. For a team looking for something to build on, the honest answer is that the project itself says it is dormant, and the last push was on 2026-05-14.

## Conclusion

Magmide is worth reading as a design document rather than adopting as a dependency, because its split Logic and Host architecture and its argument about Iris style separation logic are a clear statement of what a systems oriented proof language would need, and the repository is small enough to read in an afternoon. It is not something to build on today, since the README describes the repository as dormant and the files as rough notes and exploratory theorem proving, and no licence is stated. Before spending time on it, read README.future.md alongside README.md to see how the author frames the current state, and check the licence situation directly, because a project with no stated licence cannot be used or redistributed by anyone else.

## FAQ

### What is Magmide?

It is a dependently typed proof language intended to make provably correct bare metal code possible for working software engineers, built on a split Logic and Host architecture where a dependently typed logic verifies an imperative host language that also implements the logic itself.

### Is Magmide ready to use?

No. The README states that Magmide is dormant for now as the author rethinks what it could or should be, that the repository is still very early and rough, and that it is mostly notes, speculative writing and exploratory theorem proving.

### What is the split Logic and Host architecture in Magmide?

It separates software thinking into two languages: Logic, the dependently typed lambda calculus of constructions where types are defined and proofs are conducted, and Host, the imperative language that runs on real machines. The two must be symbiotic, with Logic used to make assertions about Host and Host implementing both itself and Logic.

### Why does Magmide focus on separation logic?

The README argues that separation logic allows verification of practical imperative code rather than outlawing mutation, that Rust was inspired by it, and that Iris is a fully powered separation logic used so far only in academic papers that analyse manual transcriptions of source code rather than the code itself.

### How do you build the Magmide sources?

The justfile has a test target that runs cargo test and dune runtest, a build target that runs make inside the theory directory, and a fullbuild target that first generates a Coq makefile with coq_makefile from the _CoqProject file before compiling.

## Sources

- [Issues](https://github.com/magmide/magmide/issues)
- [magmide/magmide on GitHub](https://github.com/magmide/magmide)
- [README](https://github.com/magmide/magmide/blob/main/README.md)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/magmide-magmide