Work
One manifest lists page revisions, so a crawler can check what changed before downloading pages again.
The recorded run checks three pages across three visits, including audits of cached pages.
See a recorded runHow do I build ries-rs? It depends which build you need.
- Native tool ·
.repo cargo build --release --locked- Browser package ·
package.json npm run build
RamenOS
An experimental OS in Rust for giving agents specific resources without giving them a whole shell.
Public pre-alpha
RamenOS boots on two architectures in QEMU. I’m still building the agent-task demo.
The September 17 checks cover x86_64, aarch64, and services running on the host computer.
What runs so farlean-xray
Inspect the assumptions behind a Lean declaration, and what the audit actually checked.
In Progress
Demo.conclusion↓ depends onDemo.starting_point
Recorded deep audit of a demonstration fixture.
Follow the assumption →5 recorded checks · C/D scope
Build → statement comparison → axiom closure → Nanoda → Lean replay
Each result has a different scope. Manual correspondence review remains separate.
Inspect the receipt →107,899 bytes → accepted107,898 bytes → rejected
One byte separates two recorded strict-decoding results.
Inspect the missing byte →