Inspiration
AI can help cybersecurity investigators process large amounts of digital evidence, but it can also make convincing claims that the evidence doesn't fully support. In digital forensics, confusing two USB devices or misinterpreting a timestamp can lead to an incorrect account of what happened.
We were inspired by tools like Magnet AXIOM and Mulder, which help investigators reconstruct events from digital artifacts. We wanted to take this further by making AI-generated forensic findings independently verifiable.
What it does
CONAN-F (CONsistent ANalysis in Forensics) is an AI-powered forensic investigator that uses Lean 4 to check claims against digital evidence.
The AI examines extracted records, investigates suspicious activity, and proposes findings. Each claim is converted into a formal representation and checked by the Lean kernel. Accepted claims receive reproducible proof certificates, while rejected claims include explanations of which conditions failed.
Our forensic workbench lets users explore evidence relationships, inspect timelines, trace findings to their original artifacts, review proof certificates, and generate investigation reports.
How we built it
We built the backend in Python, using forensic extraction tools to process disk images, Windows Registry records, browser history, file metadata, and removable-device activity.
We designed a structured claim language using five logical operations: is, val, link, before, and both. These operations form the basis of our Lean 4 verification process.
The AI investigator uses restricted tools to search evidence and submit claims. Python generates the Lean code, and the kernel determines whether the claims satisfy the defined rules.
We built the frontend using HTML, CSS, and JavaScript, creating an interactive forensic workbench with evidence graphs, proof inspection, and customizable reports.
Challenges we ran into
Our biggest challenge was connecting AI reasoning to formal verification. Forensic evidence is often incomplete or ambiguous, and translating complex conclusions into precise logical statements requires careful design.
We also encountered difficulties with timestamp uncertainty, conflicting device identifiers, large evidence datasets, and ensuring that verified findings actually answered the intended investigative tasks.
During evaluation, we discovered that a mathematically valid certificate could still be associated with an incomplete or incorrectly structured answer. We added stricter claim-to-answer requirements and improved our handling of unresolved evidence.
Accomplishments that we're proud of
- Built an end-to-end forensic investigation pipeline connecting AI agents, digital evidence extraction, Lean 4 verification, and a visual investigation workbench.
- Extracted over 335,000 forensic records from the NIST CFReDS Data Leakage Case.
- Independently verified all 473 certificates in our saved demonstration report.
- Rejected 24 out of 24 deliberately false claims in our regression tests.
- Built a visual proof graph that traces findings back to their source artifacts and distinguishes verified observations from uncertain interpretations.
We are especially proud that investigators can inspect the exact logical conditions behind a finding and independently reproduce its proof.
What we learned
We learned how formal verification can be integrated into an AI agent workflow, how forensic tools reconstruct events from disk artifacts, and how difficult it is to evaluate AI reasoning reliably.
Our initial controlled comparison also showed that Lean feedback did not automatically improve overall answer accuracy. This helped us identify a limitation: verifying individual claims does not establish that an investigation is complete or that every conclusion has been interpreted correctly.
That finding has shaped how we're continuing to improve CONAN-F.
What's next for CONAN-F
We want to improve how CONAN-F responds when evidence is insufficient. Instead of simply rejecting a claim, the investigator should identify what additional evidence could resolve the uncertainty and guide further investigation.
We're also working toward broader forensic artifact support, better evidence interpretation, and more complete investigations across different cases.
Our next evaluation goal is to compare CONAN-F against Mulder and AI investigators without formal verification under consistent conditions, measuring both accuracy and evidence coverage.
Ultimately, we want to make AI-assisted digital forensics easier to inspect, challenge, and verify.
