I used AI to organize my thoughts, but they are my thoughts, I just have adhd. I hope this doesn't stop you from reading the most important and underrated containment architecture in existence and being one of the the earliest adopters of the world's first wire-level interposer containment architecture, fully mathematically and silicon route verified.

AI safety sandboxes today are just software wrappers running on the same machine as the model. If an autonomous agent or an attacker gets root access in the operating system or even just triggers a quick warm reboot, they can turn those software guardrails off from the inside. This requires containment security at the interposer level.

I built a physical hardware lock that sits underneath the operating system directly on the server's memory wire. Because the rules are enforced by the chip itself instead of software, a compromised host OS can't widen its own memory permissions or quietly copy out model weights. Somebody has to physically walk up to the server rack and pull the power cord to reset the lock. It also runs at full wire speed without eating up gigabytes of server memory for lookup tables.

The chip logic, math proofs, and cloud hardware tests are already done. I'm asking for $7,500 to $15,000 right now ($35k stretch goal) for two very immediate things: replacing my only laptop, which is dying under the load of heavy chip-synthesis and proof runs, and paying 2 to 3 months of basic family bills here in Virginia Beach. That buys me the time to wrap this into a free, easy-to-run testing tool for AI safety labs this winter instead of dropping the project to take a regular full-time job.

- Code (GitHub): https://github.com/spectralsystems/spectral-cxl-flit-sanitizer

- Paper (Zenodo): https://doi.org/10.5281/zenodo.24047902

- Site & live test data: https://spectralsystems.org

# What are this project’s goals? How will you achieve them?

The hard part of writing the chip logic, proving it in Lean 4, and testing it on real AWS F2 cloud FPGAs is already finished. I'm not promising milestones i may or may not deliver, I did all of this and THEN sought funding. Over the next 8 weeks, I want to turn those raw hardware pieces into a straightforward open-source (Apache-2.0) test harness. Most AI safety evaluators (groups like METR, AISI, or Apollo) are software teams, not FPGA engineers, so they need a one-command tool they can run to see how hardware containment holds up against kernel escapes compared to standard container sandboxes.

Under the hood, the chip does a few things software can't:

- One-way permission ratchets (BAR0 0x00/0x08): The permission registers use a bitwise-AND latch reg <= reg & wdata) wired to the cold power-on reset pin instead of warm PCIe resets. Once you lock down an agent's memory range, even a full Ring-0 kernel exploit can't open it back up without a cold power cycle.

- Weight-theft clamping on the read path (CSR 0x58): The read path clamps floating-point mantissas in hardware (using 0 extra LUTs) so an attacker or rogue process can't reconstruct model weights through repeated queries, and unauthorized writes get scrubbed into harmless no-ops with flat timing.

- Proofs down to the silicon truth tables: I proved the logic in Microsoft Lean 4 Init.Prelude, 0 sorry, 0 axioms) all the way down to the actual 16nm AMD xcvu47p LUT6_2 configuration bitmasks. You don't have to take the commercial chip compiler on faith.

# How will you know it worked?

Two months from now, an evaluator who clones the GitHub repo will be able to run the whole test suite out of the box:

1) An Apache-2.0 benchmark that throws simulated root kernel escapes, warm PCIe resets, and weight-extraction queries at standard Docker/Linux sandboxes vs. our Kubernetes webhook spectral-operator, 1.36 ms block time) and hardware ratchet.

2) Live hardware traces recorded on 16 GB HBM2 cloud FPGAs (AWS f2.6xlarge, agfi-08becf3b40b169674), where we fire 100,000 bad DMA bursts at the bus and show 100% victim memory survival 0xAAAAAAAAAAAAAAAA), 99.2% link goodput for clean traffic, and zero PCIe bus lockups.

3) A quick local check lake build and make all) that finishes in under a minute on a normal machine, verifying all 30 Lean 4 theorem groups and running a 40,000-slot fuzzer against the behavioral model.

# How will this funding be used?

I'm down to one aging laptop, and it is starting to fail. Running 30 tactic-free Lean 4 proof builds, SAT equivalence checks, and local AMD Vivado place-and-route passes eats a ton of RAM and maxes out CPU thermals for hours at a time. At the same time, my personal savings runway for household bills is just about gone.

Here is where the money goes:

Immediate minimum budget ($7,850 – $13,850):

- $2,450 for a replacement high-RAM (64–128 GB) laptop/workstation. That lets me run Vivado synthesis, SAT miters, and Lean 4 builds locally without the machine crashing—and saves me from burning grant money on expensive hourly cloud servers just to compile code.

- $4,800 to $10,800 for 6 to 8 weeks of basic family living expenses (mortgage/rent, groceries, utilities in Virginia Beach) so I can work full-time on packaging spectral-operator and the open-source escape benchmark right now.

- $600 for AWS f2.6xlarge FPGA spot instances ($0.24–$1.50/hr) to run the public hardware red-team tests.

If we hit the full $15,000 – $35,000 target:

- That covers 3 to 4 months of living runway so I can also finish the open-source Rust/C BAR0 verification library, the CSR 0x58 proof-carrying egress airlock for cluster inspection, and direct vLLM multi-tenant integration.

# Who is on your team? What’s your track record on similar projects?

Just me—Eric Murphy eric@spectralsystems.org), based in Virginia Beach, VA (Spectral Systems LLC). My background is in systems engineering, hardware architecture, and formal verification. Because I work solo, I built the whole stack end-to-end: the finite-field math, the Lean 4 proofs, the SystemVerilog RTL, the AMD Vivado 16nm FPGA builds, the 7nm ASAP7 standard-cell layout, and the Linux/Kubernetes driver code.

Everything in the repo right now was built solo over the last few months:

- 30 theorem groups proved in pure Init.Prelude Lean 4 0 sorry, #print axioms completely empty), including gate-level translation validation of the placed 16nm LUT6_2 truth tables.

- Post-route 16nm FPGA timing closure on AMD Virtex UltraScale+ xcvu47p (1,585 core LUTs, 0 Block RAM, 0 DRC errors) plus a routed 7nm ASAP7 layout 0.003335 mm²).

- Hardware-in-the-loop DMA testing on live 16 GB HBM2 silicon on AWS EC2 f2.6xlarge agfi-08becf3b40b169674) across 100,000 sub-flit slots.

# What are the most likely causes and outcomes if this project fails?

Since the circuit is already routed, proved in Lean 4, and tested on AWS F2 FPGAs, there isn't really a technical risk that the hardware won't work.

The real risk is simply running out of runway or having my laptop die mid-build this month. If I have to stop working on this next week and take unrelated full-time contract or payroll work to pay family bills, the project stays in its current state: a working chip design and a dense math paper that software-focused AI safety researchers won't know how to set up or test on their own. Even if that happens, all 30 Lean 4 proof groups formal_lean4/) and the Zenodo paper 10.5281/zenodo.24047902) are already online under Apache-2.0 and won't go anywhere. A quick $7,500–$15,000 grant keeps me on this long enough to make the tools usable for everyone else.

# How much money have you raised in the last 12 months, and from where?

$0. I paid for the cloud FPGA runs, tooling, and living costs out of my own savings while unemployed. I recently sent in fast-grant applications to BlueDot Impact and the GTR AI Safety Fund, and haven't heard back yet. Even hitting the $5,000–$7,500 minimum here buys the replacement laptop immediately and gives me the breathing room to ship the benchmark.