Tessera
Folgen

opale !!

@n1ark.acouphene.net

compsci phd + soteria rust @ https://soteria-tools.com writing + dev @ https://acouphene.net myself @ https://n1ark.com she/her 🏳️‍⚧️

253 Posts163 Follower154 Folgt
opale !!@n1ark.acouphene.net · 2w ago

i wrote a blog post about a cool optimisation i did to make quadratic behaviour linear while remaining sound !! its a mix of pretty technical GC details and theoretical Rust stuff, which is the best of mixes imo, go read it !! ! !! soteria-tools.com/blog/meta-ga...

Meta Garbage Collection: Using OCaml's GC to GC Rust - Soteria

Tracking Rust's aliasing model can be quadratically expensive if done naively. Learn how we fixed this in Soteria Rust by doing meta garbage collection.

soteria-tools.com

opale !!@n1ark.acouphene.net · last mo.

<work> you must be DYING to know how symbolic execution relates to ai ! well wait no more because there was a paper about it and we explain what the paper is about in our latest blog post !! ai !! llms !!! all the stuff people scream about !!! wow ! </work> soteria-tools.com/blog/teachin...

Teaching AI to Reason About Software - Soteria

A team at AWS taught a small language model to catch bugs in C by training it on Soteria’s symbolic execution traces, beating a model four times its size. We look at what they did and why it matters.

soteria-tools.com

opale !!@n1ark.acouphene.net · last mo.

i hate british sliced bread i bought this pack FIVE (5) days ago and it's already gone mouldy how is anyone meant to finish a pack of bread, im sorry i dont eat >2 slices a day !!

rain 🌦️@sunshowers.io · 2mo ago

Update: iddqd is now formally verified*! * with limitations that are fundamental to this kind of formal verification, making it a complement to the existing layers of validation For more, see: oxide.computer/blog/iddqd-u...

Update 2026-06-16: Since publication, we’ve used Soteria to verify that iddqd's no-duplicate-index invariant holds under arbitrarily adversarial Hash and Ord implementations. Soteria is similar to Kani in spirit, though with different internals that make it more compatible with iddqd. Soteria is implemented as a symbolic execution engine that lets you declare points of nondeterminism in your code. (For example, within iddqd, we represent an adversarial Hash or Ord return value as nondeterministic, since we want to model adversarially bad user code.) Then, it: Compiles the Rust program into a form suitable for formal verification. Interprets this form until it reaches a point of nondeterminism, treating each such point as a symbol rather than a concrete value. Branches at each point where control flow depends on a symbol, validating that there is no UB and that the invariants specified by the program are upheld. A lot of the cleverness lies in how the possibility space is collapsed down to something manageable. For example, Soteria doesn’t have to enumerate every possible Hash value; rather, it only has to fork in places where control flow depends on the Hash value.
rain 🌦️@sunshowers.io · 2mo ago

iddqd, or the hardest kind of unsafe Rust. My first post for the @oxide.computer blog! Goes deep into the pitfalls of unsafe Rust and how to reason about it. A lot of labor went into the post -- please have a read! oxide.computer/blog/iddqd-u...

gabby@fullmoon.id · 2mo ago

The moral of the story is that human attention is the bottleneck, not the number of agents because correctness is definitionally what the human intended to happen If you can't be bothered to spare any attention to the process you will get incorrect results no matter what harness you are using

gabby@fullmoon.id · 2mo ago

The evolution of a prompt engineer: - I ask an agent to perform an action but performance is inconsistent - I ask an agent to better ask another agent to perform an action - I ask an agent to check the other agent’s work - I spin up N agents in parallel to do the task and hope that one succeeds …