m1el

Translating your program to Rocq is vastly easier than to write a proof for a binary.

LowIRSSA looks way more like SSA-WASM than assembly

My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code".

We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.

Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...

I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost.

We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically.

On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected!

The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification".

I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time.

My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet.

What I have so far:

- one (non-optimized) compiler step which is formally verified

- three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR

https://github.com/m1el/riscv-fv-bootstrap

The project is in quite a bad shape, and I am trying to improve my skills in that direction.

https://github.com/pipecat-ai/nemotron-january-2026/

discovered through this twitter post:

https://x.com/kwindla/status/2008601717987045382

https://huggingface.co/nvidia/nemotron-speech-streaming-en-0...

https://github.com/m1el/nemotron-asr.cpp https://huggingface.co/m1el/nemotron-speech-streaming-0.6B-g...

https://github.com/m1el/samaras/blob/master/src/xorshift128....

1) Select All (most likely followed by the copy) 2) Type the answer 3) Make an obvious mistake when they type else block, before the if

Of course this will change in the future, with more interactive models, but people who use ChatGPT on the interviews make a disservice to themselves and to the interviewer.

Maybe in the future everybody is going to use LLMs to externalize their thinking. But then why do I interview you? Why would I recommend you as a candidate for a position?

Here's my solution, which also uses pdep/pext

Edit: the post says open-source models.

2.1 Define FlameGraph

    Frame = something that identifies function/location in the code
    Stack = Vec<Frame>
    FlameGraph = Map<Stack, Real>
    FlameGraphPositive = Map<Stack, RealPositive>

    FlameChart = Vec<{ start: Real, flame_graph: FlameGraphPositive }>
    # such that the start values are strictly ordered
    fn to_flamegraph(flame_chart: FlameChart) -> FlameGraphPositive {
        flame_chart
            .map(|{ start, flame_graph }| flame_graph)
            .sum() 
    }

    FlameChart = Vec<{ end_time: RealPositive, stack: Stack }>
    # such that sampling starts at 0 and Vec is strictly ordered by end_time
    fn to_flamegraph(flame_chart: FlameChart) -> FlameGraphPositive {
        let mut start = 0.0;
        flame_chart.map(|{ end_time, stack }| {
            let elapsed = end_time - start;
            start = end_time;
            FlameGraphPositive::from_stack(stack, elapsed)
        }).sum()
    }

    # a,b: FlameGraphPositive
    fn diff(a, b) -> FlameGraph;
    # such that a + diff = b
    # diff: FlameGraph
    # add, sub: FlameGraphPositive
    fn to_positive(diff) -> { add, sub };
    # such that diff = add - sub

    # a,b: FlameGraphPositive
    fn diff_metric(a, b) -> RealPositive {
        diff(a, b).size() / (a.size() + b.size())
    }
    # diff_metric(a, b) \in [0, 1]^Real

Using Hotelling T^2 Test, the author defines a metric, which takes sampling variance into account, and allows to detect performance regression, even when the sampling profile is noisy. (you'd have to read the paper for the exact method)

The code for this test is here: https://github.com/P403n1x87/flamegraph-experiment/blob/04db... https://github.com/P403n1x87/flamegraph-experiment/blob/04db...