Jan 12, 2026

FV-Deception

Lee Wall

I ran a set of experiments to see if frontier LLM's could intentionally generate formal verification specs that slightly diverge from the natural-language semantic intent, and whether other models could reliably catch this divergence.

Reviewer's Comments

Reviewer's Comments

Arrow
Arrow
Arrow

Targeting deception in formal specifications is a valuable and neglected direction. The finding that Opus catches fewer of its own bugs than Sonnet is interesting, and I'd like to see whether this replicates with a larger attacker-defender capability matrix. Including concrete examples of deceptive specifications would also help readers interpret what's actually happening.

I am not familiar with the literate on FV, but from what I (+Claude) can tell after digging around there is very little existing work done on this specific problem, and it seems like very important work for the FV field to me. For me this was in shot for a top score on impact if the conclusions were more explicit - what is the so what? What does this really mean and what do we now need to do? It seems like you are very thoughtful about this space, and I was eager to see more of your thinking and takes!

The execution had room for improvement. The sample size is quite small. The methodology mentions 9 combinations of model attacker/defenders, but only the data and conclusions on using Opus as an attacker was discussed. No analysis of successful / unsuccessful attempts at attacks. I found it hard to really have faith in the (important!) conclusions with these limitations.

The things that the report communicates are all clean. You know how to write clearly. Well written and argued. I would have liked to see more detail and coverage of the data and experiments that were done.

I hope you continue with this area of work.

Cite this work

@misc {

title={

(HckPrj) FV-Deception

},

author={

Lee Wall

},

date={

1/12/26

},

organization={Apart Research},

note={Research submission to the research sprint hosted by Apart.},

howpublished={https://apartresearch.com}

}

Recent Projects

View All

Feb 2, 2026

Markov Chain Lock Watermarking: Provably Secure Authentication for LLM Outputs

We present Markov Chain Lock (MCL) watermarking, a cryptographically secure framework for authenticating LLM outputs. MCL constrains token generation to follow a secret Markov chain over SHA-256 vocabulary partitions. Using doubly stochastic transition matrices, we prove four theoretical guarantees: (1) exponentially decaying false positive rates via Hoeffding bounds, (2) graceful degradation under adversarial modification with closed-form expected scores, (3) information-theoretic security without key access, and (4) bounded quality loss via KL divergence. Experiments on 173 Wikipedia prompts using Llama-3.2-3B demonstrate that the optimal 7-state soft cycle configuration achieves 100\% detection, 0\% FPR, and perplexity 4.20. Robustness testing confirms detection above 96\% even with 30\% word replacement. The framework enables $O(n)$ model-free detection, addressing EU AI Act Article 50 requirements. Code available at \url{https://github.com/ChenghengLi/MCLW}

Read More

Feb 2, 2026

Prototyping an Embedded Off-Switch for AI Compute

This project prototypes an embedded off-switch for AI accelerators. The security block requires periodic cryptographic authorization to operate: the chip generates a nonce, an external authority signs it, and the chip verifies the signature before granting time-limited permission. Without valid authorization, outputs are gated to zero. The design was implemented in HardCaml and validated in simulation.

Read More

Feb 2, 2026

Fingerprinting All AI Cluster I/O Without Mutually Trusted Processors

We design and simulate a "border patrol" device for generating cryptographic evidence of data traffic entering and leaving an AI cluster, while eliminating the specific analog and steganographic side-channels that post-hoc verification can not close. The device eliminates the need for any mutually trusted logic, while still meeting the security needs of the prover and verifier.

Read More

Feb 2, 2026

Markov Chain Lock Watermarking: Provably Secure Authentication for LLM Outputs

We present Markov Chain Lock (MCL) watermarking, a cryptographically secure framework for authenticating LLM outputs. MCL constrains token generation to follow a secret Markov chain over SHA-256 vocabulary partitions. Using doubly stochastic transition matrices, we prove four theoretical guarantees: (1) exponentially decaying false positive rates via Hoeffding bounds, (2) graceful degradation under adversarial modification with closed-form expected scores, (3) information-theoretic security without key access, and (4) bounded quality loss via KL divergence. Experiments on 173 Wikipedia prompts using Llama-3.2-3B demonstrate that the optimal 7-state soft cycle configuration achieves 100\% detection, 0\% FPR, and perplexity 4.20. Robustness testing confirms detection above 96\% even with 30\% word replacement. The framework enables $O(n)$ model-free detection, addressing EU AI Act Article 50 requirements. Code available at \url{https://github.com/ChenghengLi/MCLW}

Read More

Feb 2, 2026

Prototyping an Embedded Off-Switch for AI Compute

This project prototypes an embedded off-switch for AI accelerators. The security block requires periodic cryptographic authorization to operate: the chip generates a nonce, an external authority signs it, and the chip verifies the signature before granting time-limited permission. Without valid authorization, outputs are gated to zero. The design was implemented in HardCaml and validated in simulation.

Read More

This work was done during one weekend by research workshop participants and does not represent the work of Apart Research.
This work was done during one weekend by research workshop participants and does not represent the work of Apart Research.