Some current projects

LeanExe is a system for developing fully verified executable programs. LeanExe is based on a compiler of a subset of Lean. The compiler itself is implemented in Lean, and it emits WASM. Those output artifacts are proved correct based on extensions to the Talos formal model (in Lean) of WASM and the source program itself (written in that Lean dialect). Proofs about the source Lean program should be provable for the compiler output. WASM verification includes checking various bounds, including heap and stack use. We have a several examples, including this two-dimensional Euler Riemann problem and this fully-verified GPT-2, which includes formal verification of GPU code.

VQ is a sytem for verifying quantum algorithms. We've used VQ internally to develop and verify the lowest logical qubit algorithm for secp256k1 Discrete-Logarithm Algorithm (ECDLP). Currently we are using VQ to develop and verify efficient ECLDP and elliptic curve point addition algorithms for various logical qubit counts, Toffoli counts, and other metrics and bounds.

Agent District Court (ADC) is a system for automatic dispute adjudication based on the U.S. Federal Rules of Civil Procedure. ADC's core procedural engine is implemented in Lean, and ADC has a wide range of theorems about that procedure. Since many ADC cases are fact-intensive, this system bridges our formal verification and applied epistemology work. Here's is an example of an ADC case related to a disputed prediction market resolution.

ACE is an agent communication engine inspired by Gelernter's Linda and tuple spaces. ACE supports full patterns and structured matching, expiration, explicit deletes, and other capabilities to enable very advanced inter-agent communication.

CAP is a system for "Communicating Agent Processes" (in the spirit of communicating sequential processes). CAP is basically a harness designed specifically for hosting thousands of concurrent agents with powerful coordination primitive operations, including ACE operations. CAP encourages agents to develop and evolve their own ways of organizing and collaborating. Situational awareness and other detailed world observation and analysis are important application areas for CAP. One CAP process can observe and even control (debugger-style) another CAP process and its agents.

Several of these sysems incorporate evolving knowledge bases as critical components. These knowledge bases grow over time, and they blend the traditional roles of code and data. For example, LeanExe has support for modular knowledge bases called LTGs. "LTG" stands for "lemmas, tactics, and guidelines". The LeanExe compiler emits annotations that can facility the identification of LTG techniques that are useful to prove properties of the emitted artifacts. Similarly CAP can distill modes of communication and collaboration that subsequent CAP processes can consider, use, and develop further.

marXiv is our own little personal arXiv-like service, which we run internally. We publish selected papers here. This service includes a pretty mean AI editor based on frontier models at very high levels of effort. Together with our specific and also somewhat mean style guide and requirements, our agents usually iterate based on the reviewer remarks to improve submissions incrementally.