Reasoning about software at the level of the machine.
The Low-Level Reasoning Machine lifts higher-level, provably-equivalent models from machine code — then verifies their security properties with machine-checked proofs. No source code required.
Low-level reasoning is motivated by settings where source or library code is unavailable, where build processes have decayed, and where errors must be patched fast — while keeping the trusted computing base small (it excludes compilers, linkers, and runtimes). Formalizing instruction-set semantics is far more tractable than formalizing programming-language semantics, which is what makes verifying software from the binary up possible. Read the full approach →
Instruction semantics
Formal, machine-validated semantics for x86 and ARMv8 — recovered automatically rather than written by hand.
Verified decompilation
Lifting stripped binaries to assembly, IR, and C that is provably equivalent to the original.
Weird machines
Reasoning about the weird machines behind memory-corruption exploits, via formal memory-usage certificates.
