From borrowing to bytes
Memory safety from Rust borrowing to native-code verification. Song's first x86-64 multiplication has a Lean proof; the full compiler and kernel are ahead.
In 2019, memory safety errors accounted for 76% of Android's reported vulnerabilities. By September 2024, Google put that share at 24%. Its November 2025 update reported it below 20%. A large part of the strategy was writing new code in memory-safe languages, including Rust, while keeping much of the existing C and C++. The 2024 report and the 2025 update describe the data.
The share caused by memory safety errors
These are familiar mistakes. Read past the end of a buffer. Use an object after it has been freed. Keep a pointer into an allocation which somebody else has moved. The difficult part is keeping them absent while the programme changes.
The economic cost goes well beyond paying a programmer to fix the line. In 2017, WannaCry spread through a flaw in Windows file sharing. The UK health department estimated that it cost the NHS £20 million during the outbreak and another £72 million to restore data and systems. Appointments and operations were cancelled, and some emergency departments had to send patients elsewhere. Its account of the attack makes the cost fairly concrete. Other people lose the use of a service while we repair the software underneath it.
There are national security consequences too. Australia's cyber security agency records Volt Typhoon exploiting an unpatched Fortinet firewall. The flaw was a buffer overflow in its remote-access service. In its 2023–24 threat report, ASD describes the US assessment that this China-backed group was establishing access to critical infrastructure so it could disrupt services during a crisis or conflict. A memory error in a device meant to protect a network can give somebody a way into it.
Then there's sovereignty. Can we inspect, build, repair and replace the software our hospitals, businesses and governments depend on? Who can keep it running if a supplier stops supporting it, changes the terms or withdraws access? Germany's Centre for Digital Sovereignty is building open-source alternatives and migration routes for public administration to reduce those dependencies. To me, sovereignty includes having the people and tools to maintain the systems ourselves. That takes code we can work on, knowledge we can retain and alternatives we can actually use.
I want to be able to change a programme without manually rebuilding its safety argument every time. Song is my attempt to carry more of that argument through the language, compiler and operating system, down to the bytes which execute.
Maintaining the same mistake
Heartbleed was a missing bounds check in OpenSSL's handling of a heartbeat message. It could expose up to 64 KB of memory. A length supplied by the other side of a connection was allowed to describe more data than the message actually contained.
Nine years later, curl's SOCKS5 overflow showed how a maintenance change can break an existing safety decision. Hostnames longer than 255 bytes were supposed to be resolved locally, instead of sent to the proxy. When the handshake was converted from a blocking function into a non-blocking state machine, a local variable could lose that decision between calls. A slow handshake could then send an over-long hostname down the copy path. With a sufficiently small destination buffer, that became an overflow.
That is a miserable thing to maintain. A decision made before waiting for the network has to survive when the function resumes. The parser, the protocol limit, the buffer size and the state machine all have to agree. Each can look reasonable in isolation.
Consider a smaller maintenance problem. A programme keeps a pointer to the first element of a growable buffer. Then the buffer grows. If growing it moves the allocation, the saved pointer refers to the old allocation. An index of zero can pass every length check and still access freed memory. The length was never the problem.
In safe Rust, the straightforward version is rejected:
let mut values = vec![1, 2, 3];
let first = &values[0];
values.push(4);
println!("{first}");push needs mutable access to the vector while first still borrows it. Rust refuses that combination, whether this particular push would move the allocation or not. The Rust book explains this case.
In a larger C or C++ programme, the growth might happen through a callback, on an error path, or after a helper function changes. The programmer has to find every surviving pointer and establish that it remains valid. A comment saying the buffer won't move is another thing to keep correct.
The fix can be a line. Establishing that the same mistake isn't still elsewhere means following every caller, lifetime and failure path. Then somebody changes one of those paths. We have built a lot of software whose safety depends on people repeatedly remembering the same facts, across code they don't own.
So we add reviews, static analysis, fuzzing, sanitizers and regression tests. A sanitizer can catch an invalid access on a run that reaches it. A regression test can keep a known failure fixed. Neither makes every future use of that pointer valid. Somebody still has to maintain the relationship between the object and every operation which uses it.
The work continues after a fix. Find which products carry the dependency. Backport the patch. Check what broke. Get the update to machines whose owners may never have heard of the library. CISA's memory-safety roadmap guidance names that recurring cost to manufacturers and users. Calling all of this programmer discipline doesn't make it scale.
Why Rust is moving into the kernel
There is already a practical response. Linux has Rust support, and the Rust for Linux project lists mainline users including Android's Binder driver and GPU drivers. The migration has to work alongside the C kernel people already have.
The kernel documentation describes the structure: Rust drivers use abstractions which wrap the C interfaces. The wrappers have to get allocation, lifetimes, locking and cleanup right. Their users can then work within the rules Rust checks. That concentrates difficult reasoning in a smaller part of the system, but somebody still has to establish that those wrappers are sound.
This is also the direction of government guidance. In December 2023, CISA, the NSA, the FBI and partner agencies, including Australia's cyber security authorities, recommended published roadmaps towards memory-safe languages. Their January 2025 guidance recommended memory-safe languages for new product lines and prioritised migration plans for existing products. Rust is one option. The recommendation is to prevent the class of error at its source.
The research is more specific about what that requires. Jung and colleagues' RustBelt paper, POPL 2018, gives a machine-checked safety proof for a model of a substantial part of Rust. It also sets out the obligations an internally unsafe library must satisfy to provide a safe interface. Putting a safe function around raw pointers doesn't establish those obligations by itself.
Li and colleagues' Rust-for-Linux study, USENIX ATC 2024, examined six drivers, their code and development discussions. It found benefits from Rust, alongside bugs in abstractions and difficulties fitting ownership into existing kernel conventions. That study describes the code at the time; it isn't a count of today's kernel vulnerabilities. It does show where the maintenance burden goes when two languages have to share a system.
There is evidence that reducing that burden helps ordinary development too. Google's November 2025 Android report found roughly four times lower rollback rates for medium and large Rust changes than C++ changes, and about 25% less time in review. These are observations from Google's development process, rather than a controlled comparison of identical programmes. They are still useful numbers for anyone tired of shipping a change and spending the next week undoing it. The report describes the comparison.
For Song, I want to carry that further. The buffer's extent, its owner and the authority to write it need to survive compilation and become restrictions on what executes.
An address and an object
Allowed by this rule. The write reaches buffer B.
Take two buffers, eight bytes each. Put them next to one another inside a sixteen-byte region. A four-byte write starting at byte six touches the last two bytes of A and the first two bytes of B. It stays inside the region throughout.
This is a small example of a much larger problem. Knowing that an address is inside memory doesn't tell me that this operation is allowed to touch the object at that address.
In C I can write a function like this:
void write_byte(unsigned char *p, size_t i, unsigned char value) {
p[i] = value;
}The function receives a pointer, an index and a byte. The length of the object isn't an argument. I can add a length and a check, but then I need to keep the pointer, the length and the object they describe in agreement. The caller and the function share that responsibility.
The equivalent Rust function takes a slice:
fn write_byte(p: &mut [u8], i: usize, value: u8) {
p[i] = value;
}The slice carries the extent of this buffer. The mutable borrow constrains other access to it, and the indexing operation checks its boundary. Those facts have become part of the language's treatment of the object. Unsafe code and foreign interfaces still need their own argument.
C predates x86. Ritchie's account places its development in early Unix, on the PDP-11. It gave programmers a compact way to work with the machine's memory and instructions. Arrays, pointers and the cost of their implementation were closely related design concerns.
On an ordinary x86-64 system, I can place a numeric address in a register and use it to read or write memory. Paging and privilege levels control access to mapped regions. They don't attach the length and lifetime of every C object to each address. Two objects can occupy the same writable page. Crossing from one into the other needn't cause a hardware fault. Intel's architecture manuals describe those mechanisms.
So a C buffer overflow isn't necessarily a programme doing something the processor refuses. It can be a processor doing precisely the requested access after the programme has left the behaviour C defines for it. The optimiser also assumes the source programme obeys C's rules, which makes reasoning from an accidental out-of-bounds access particularly unhelpful.
The Turing and von Neumann models are useful abstractions for computation and stored programmes. They don't, by themselves, tell an implementation which object an address belongs to, who may modify it, or when it stops existing. We have to put those distinctions somewhere.
Rust puts many of them into the language. RISC-V gives us an open, modular instruction set on which we can build hardware and extensions. Its base load and store instructions still operate on addresses. Choosing RISC-V doesn't automatically give a programme object bounds or ownership. Those require another mechanism.
What the existing systems establish
There are already substantial answers to parts of this problem. They operate at different levels, so I want to be fairly specific about what I take from each.
seL4 proves that the kernel implementation follows its specification. On supported configurations it also connects the C implementation to the binary. Its security proofs establish properties such as integrity and isolation under the system's access rules. That is much stronger than testing a kernel and finding no buffer overflows. The proof overview describes the layers and their coverage.
The cost is building and maintaining that connection as the implementation and supported configurations change. Applications still need their own correctness arguments. seL4 is a general-purpose kernel, with particularly strong reasons to use it in critical systems. My interest is in making this sort of assurance practical through a broader stack, including the things people keep changing while they develop an application.
CHERI changes what a machine pointer carries. A capability includes bounds and permissions, with hardware enforcing restrictions on how it can be used and derived. In the buffer example, a capability bounded to A can prevent the access to B even though both are in the same mapped region. Its hybrid design also provides a migration path for existing software, which matters a great deal if the objective is to run software people already have.
Bounds don't solve reuse. If an object is freed and its memory becomes somebody else's object, an old capability needs to lose its authority. CHERI's Cornucopia work addresses that with revocation. Spatial bounds and lifetime are separate obligations. Song needs both too.
seL4 and CHERI can complement one another. One establishes kernel behaviour and access policy; the other can enforce finer restrictions on machine accesses. I take the lesson from both: a grant made at the top of the system needs to remain a restriction at the bottom of it.
CompCert deals with another link. Its verified compiler passes preserve the behaviour of the C programme through to its assembly representation. That is a useful guarantee when optimisations are changing the programme's shape. The source still needs to implement the intended behaviour, and the assembler, linker and surrounding environment remain separate parts of the chain. Its manual states the guarantee and its boundary.
VxWorks and aerospace assurance bring a different sort of evidence. A real-time operating system is also concerned with scheduling, deadlines and predictable resource use. VxWorks Cert Edition supplies a platform and certification evidence for safety-critical development. That can save a project considerable work, but the application and the assembled system still have to satisfy their requirements.
In aviation, DO-178C and its formal-methods supplement, DO-333 sit within a process connecting requirements, implementation and verification evidence. NASA's software assurance work similarly treats assurance as something carried through development. Tests, reviews, analysis and proofs answer different questions within that process.
These approaches are useful because they make somebody responsible for each part of the argument. The compiler has to preserve behaviour. The kernel has to preserve isolation. The hardware has to enforce the accesses its model allows. A certification package has to supply the evidence the system's requirements call for.
For Song, I also want the ordinary development loop to remain ordinary. I want to change a function, compile it, and have the relevant obligations follow that change. Games, simulations and inference kernels are much less attractive to build if every edit creates a separate manual verification project.
How I got to Song
Song grew out of my AI research. I was working on how models store information and update their state, formalising the maths in Lean and implementing it in Rust. The algebra from that work eventually became something I wanted to build an operating system on.
I use Rust because I understand the borrow checker. The Rust book was a loose influence on Song, alongside contraction theory. I was also writing Rust kernels for SPIR-V and Vulkan as an alternative to CUDA.
How much of the start remains?
The current gap is 0.367. Every starting difference shrinks by the same factor.
Eleven states start at different values and receive the same changing input. With contracting dynamics, the bundle narrows. The gap between any two states shrinks at a known rate. The other cases show why receiving the same input isn't enough: the starting difference can remain or grow.
Slotine and Lohmiller's contraction theory gives a way to establish convergence from the behaviour of nearby trajectories. The useful part for me was having a condition on the dynamics, instead of collecting examples of states moving closer together.
Convergence doesn't establish memory safety. A system can converge while overwriting somebody else's data. But the method suggested a related question: could I choose the objects and their permitted operations so that certain bad transitions couldn't occur?
The first objects eventually crystallised into three hashmaps and one merge operation. State went into the tables. Composition went through the merge. I was convinced the entire universe was contained within it.
Anyway, it turned out I was working mostly on the hyperbolic face of a well-known algebra. A boy can dream.
(2, 3) × (5, 7)
The 21 contributes positively. The result is (31, 29).
Gen2 followed a fair bit of learning about elliptic, parabolic and hyperbolic geometry. The same multiplication can describe rotations, shears and squeezes. The first essay builds that up from the beginning. Apeiron holds the algebra and its proofs; Song is where I try to make it execute as an operating system.
I was also thinking about physics and computer science more generally. A machine has finite memory, finite precision and finite time to do something. Those are useful facts to include in the model. They don't disappear because a source language lets me write an unbounded integer or a loop which never finishes.
The difficulty was following an algebraic statement all the way down to what the machine actually does. A definition can exclude an invalid state. The code implementing it still has to preserve that exclusion.
Gen1 and gen2
Generate, then follow the bytes
- Cell meaning
- Instructions
- Encoded bytes
- Modelled execution
For the first native Cell example, the proof reaches execution of the encoded bytes. Extending that chain to the compiler and kernel is ahead.
Gen1 was mostly me trying to get the algebra to carry the system. Three tables and a merge made a small foundation. There was less machinery to inspect, and the composition was appealing. But a small representation still needs a correct interpretation.
The ring example shows the problem. Masking an address into a power-of-two region keeps it inside that region. It can also turn an over-long walk into a write somewhere else in the region. If the destination belongs to a neighbouring object, the arithmetic has preserved the outer boundary and lost the property I actually needed.
I couldn't get object authority for free from a convenient address representation. It had to survive the operations which consumed that representation.
Gen2 put more of the argument into the language and compiler. Slang carried laws, specifications and explicit representations. The compiler and its provers could establish source-level conditions before emitting native machine code. That made it possible to refuse a programme for a stated reason, rather than leave every obligation to a test suite after the fact.
The small compiler also made compilation quick. In this run the archived gen2 compiler took 5.8 milliseconds for the little arithmetic workload above. Clang took 52.6 milliseconds and GCC took 135.5. Rust took 47.8. All four executables returned the expected result.
That was encouraging for the edit, compile, run loop. The small compiler does less optimisation work, and this workload has no laws to check. It tells me something about compilation latency, while kernel throughput needs its own measurement. Compile time matters when checking a change is part of making the change.
Gen2 also accumulated a second problem. The source contracts, custom provers, lowering passes and byte emitter were separate pieces of machinery. A source check could succeed while an error in a later piece changed what executed. Adding more checks around the boundary helped find defects, but each check also needed to establish that it was checking the right thing.
There was even a Lean proof kernel alongside a growing implementation of another proof language. In the gen1 tree, the Slang prover was roughly 49 times the size of that kernel. The latest history census counted 162,126 lines added or deleted, with 60.30% on paths that no longer existed. That's a lot of work spent rebuilding something we already had a small checker for. The research record explains the simpler route that came out of it.
Gen3 takes that lesson seriously. Producing a proof can be complicated; accepting it should depend on something small enough to check.
What WebAssembly checks
WebAssembly lets a programme read and write a block of memory. It checks each access against the size of that block. An access past the end stops execution. That helps protect the host running the programme. Its security model describes the check.
Now put our two buffers inside that memory. A has eight bytes, followed by B's eight bytes. Write four bytes starting at byte six of A. Two land in A. The other two overwrite the start of B. WebAssembly's memory check allows this: all four bytes are inside the block. B's data can be corrupted without the programme ever leaving its allotted memory.
For Song, I want a write to A to stay in A. The code needs to carry A's size and permission to write it. Four bytes starting at byte six don't fit, so the compiler should refuse that write. When the length comes from input, a check before writing can enforce the same limit. Checking only the starting byte would still let those last two bytes overwrite B.
The compiler then has to keep that restriction in the instructions and bytes it generates. If the source says a write stays in A, the machine code must stay in A too. That is the connection I want to establish through Song.
Gen3: following the generated bytes
(2, 3) × (5, 7)
Return (31, 29).
The first native example in gen3 multiplies two cells on the hyperbolic face. Each cell is a pair of 64-bit words. Multiply (2, 3) by (5, 7) and the result is (31, 29).
The first component is 2 × 5 + 3 × 7. The second is 2 × 7 + 3 × 5. The native programme implements those operations in ten instructions, encoded in 32 bytes.
Gen3 follows this operation through the instructions, their encoding, and execution of those bytes against the x86-64 model. The proof reaches the representation the processor is given. The diagram steps through the arithmetic; the proof covers every input in the stated word model.
The generator is part of that chain. An instruction has a meaning and an encoding, and decoding its generated bytes has to recover that instruction. Its machine transition then has to perform the operation the meaning describes. That lets us derive an implementation and check the connection, rather than keep copying encoding tables and hoping the copies agree.
Agreement within a generator is still only part of the evidence. I also need to compare its output with an independent instruction reference and the bytes which actually execute. Otherwise two pieces can share the same mistake. The native work includes those comparisons alongside the proof.
This is the main change from gen2. Proof responsibility now extends through assembly and byte encoding. The rest of the compiler and operating system is ahead.
seL4 already has a route from specification through C to binary on supported configurations. Song brings instruction generation into its own construction. The reason I chose this direction is maintenance: I want a change to the meaning or target description to produce the corresponding code and obligations together. Whether that remains practical across the full stack is something the implementation has to establish.
What Ring 0 has to cover
Think about the rings in an operating system. The code at the centre gets the most power. On x86, Ring 0 has the highest privilege and Ring 3 the lowest; Rings 1 and 2 sit between them. That controls what code may do. It doesn't prove that the code does the right thing. Intel describes the protection levels in its system programming manual.
I use four rings to organise Song's stack too. Ring 0 is the mathematical and computational foundation. Ring 1 contains reusable libraries, such as storage and I/O. Ring 2 contains applications and services. Ring 3 is what people interact with: interfaces, clients and dashboards. The inner layers don't depend on the outer ones. These are layers of the software design, rather than assignments to the processor's privilege levels.
Checked foundation
↓ trusted handwritten assemblyChecked foundation
↓ generated instructions + bytesinside the proof boundary
In gen2, Ring 0's verification stopped above the assembly core. That core was handwritten and unverified. Everything above it still depended on it doing the right thing.
Gen3 brings assembly generation into Ring 0 as well. The proof follows the operation through its instructions and the bytes they become. The first native multiplication is the concrete example. I want that foundation to carry the guarantee, rather than leave the most basic part to trust.
Bringing the existing stack with us
I don't want adopting Song to mean rewriting every driver and library by hand. I want to bring existing code across automatically, understand what it does, and keep the useful work already in it.
Take the multiplication above. A Rust function and a C function could both calculate those two results. If they use the same arithmetic rules, I'd like to translate them into the same underlying operations. Then I can analyse the calculation once and generate it for another target. A function which writes to memory also has to bring those writes with it.
That's the point of our earlier lifting work: take a programme out of the language it was written in and put it into a shared form. Subsumption takes the idea further. I want the new system to be able to absorb an existing component, analyse it and eventually replace its implementation while keeping the behaviour we need.
This is where S, K and I come in. They are three small rules for passing arguments around: I passes one through, K keeps the first and discards the second, and S puts an argument in two places. Combined with function application, these rules can express arbitrary computations. They give us a small common language to work on after translation. The first essay builds this basis from the beginning.
S f g x → f x (g x)
S supplies x to f and g, then applies f x to g x.
Once programmes have a shared form, we can look for the same structure inside them. A repeated calculation may be hidden behind different variable names, functions or source languages. Our resonance work looks for these recurring parts. Frequency analysis counts how often they occur and where they sit in the structure.
Earlier experiments also turned nesting depth into pitches and spectrograms. That let us hear and see patterns in a programme's structure. Those patterns give us places to investigate. If a calculation occurs a thousand times, can we simplify it? Can two apparently different pieces be expressed by the same term?
The next step is checking the proposed change. For pure terms, we've proved a way to pull out a repeated part and recover the original by putting it back. Real code adds another question: what does that part do? Calling a function twice can give different results if it reads a changing value, and calling it once can lose a write. Recognising the shape gives us a candidate. Preserving the behaviour is what lets us accept it.
There are already tools for parts of this journey. Charon extracts Rust into an intermediate form for analysis. Aeneas translates supported Rust programmes into functional definitions for proof assistants, including Lean. I'm using that route to connect the Rust implementation of the algebra to its Lean definitions.
The longer direction is to join these pieces: import existing code, analyse it in a shared form, check the transformations, then generate its implementation. Song's native generator supplies the last part for the operations it currently covers. Bringing whole existing stacks through that path is ahead. Universal translation deserves its own article.
Iota, and what comes next
Anyway, Slang is now Iota. I learned rather late that Slang was already a shader language, so I changed the name while moving from gen2 to gen3. Iota fits the little combinator behind the work too.
Gen2 had separate law, spec and carrier forms. Gen3 has settled on [] blocks to bring that together. When I read a function, I want to see what it does, what it's allowed to touch and why I can trust it, all in the same place. The old forms are gone; I'm still working out how the new language should feel to use. The syntax needs its own post.
I'd also like to work with it visually. If I'm working on geometry, I want to see the geometry. If I'm working on a buffer, I want to see the memory and where a write will go. I want to move between that picture and the code without having to maintain two versions of the programme.
I've been putting together an atlas of the algebra to help work out that interface. It maps the objects and how they fit together. That gives me something to work from while I figure out how to make this usable.
I'll come back to the language design, the algebra, the AI research and the cryptography in their own articles.
Both gen1 and gen2 would have been perfectly acceptable foundations for computation. They could compile and run programmes. But I come from critical infrastructure, and I wanted the safety argument to reach further.
I want to know why a system is safe, and that it stays safe when somebody changes it. That's the reason for taking gen3 all the way down to the bytes. The full compiler and kernel are still ahead. I've put the results and their evidence on a separate page for anyone who wants to look closer.