Strongest AI agent verifies only 27 of 43 code repositories
Passing 87 percent of individual proofs is not enough; whole-repo proofs stall without shared lemma libraries.
· “Vero: Can AI Agents Build Formally Verified Software Repositories?”
cs.PL
Programming Languages
Covers programming language semantics, language features, programming approaches (such as object-oriented programming, functional programming, logic programming). Also includes material on compilers oriented towards programming languages; other material on compilers may be more appropriate in Architecture (AR). Roughly includes material in ACM Subject Classes D.1 and D.3.
sort pith recommended most recent
Reported 415.8x compiler gap shrinks to 3.26x under unified test
A shared format and evaluator reveal how much of the reported gap was assumption, not compiler quality.
· “Practical Insights into Fair Comparison and Evaluation Frame for Neutral-Atom Compilers”
Three-party locks make session subtyping provably sound and complete
Scheduler probes show a type substitutes for another exactly when no error or three-party wait can arise in any context.
Type system refuses statistical claims a study can't afford
What an analysis read and how its data nests are recovered from the program, not the p-values.
· “Tacet: A Language and Type System for Automatic Statistical Validity Accounting”
Specialist-agent relay solves 62% of CodeContests tasks
A prompt-only relay with public-test checks at every step closes most of the gap to heavier systems at one-third the cost.
· “MARS: Multi-Specialist LLM Relay System for Competitive Programming”
Typing each proof step beats clicking in a classroom prover
Switching from click-to-evaluate to written evaluation steps brought exam scores back to pre-tool levels.
· “Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction”
Agent edit safety decided exactly: all safe paths
A runtime derives from its execution record what a checkpoint, fork, restore, or merge must preserve, making safety exact.
· “When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits”
Go code verified straight from //@ contract comments
A verifier proves loop invariants and termination on ordinary Go source, so students skip the second specification language.
· “VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education”
Rust's safety edge doesn't extend to web backends
Comparing Rust with Node.js and Django shows managed frameworks defend the app layer; Rust needs add-ons.
Prove layout selection NP-hard
Unified model of tensor layout choice yields exact algorithms on real graphs, separating search from cost-model error.
· “Tensor Seeks Layout: Formalizing Layout Selection for ML Compilers”
Verified verdicts on 57% of Python programs
An AI agent translates Python to Dafny with goal-blind safeguards; every verdict ships with a machine-checked proof or witness.
· “Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning”
Finitary semantics for full ground local state found
The full monad fails finitariness; its finitary submonad still denotes every program and inherits adequacy.
All async resilience fits in one nested expression
Timeouts, retries, locks, caches and rate limits become wrappers that compose without touching business logic.
· “Composable Building Blocks for Resilient Asynchronous Code”
SLICE improves contract-safe code generation by 6.58%
Separating input-validation code from function bodies raises joint success on four LLMs.
· “SLICE: Specification-Level Isolation of Contract Enforcement”
Profiling without running: 15,093x speedup on ML kernels
A compiler pass derives exact basic-block counts from tensor shapes, matching dynamic instrumentation on 73 of 78 kernels.
· “Symbolic Basic Block Profiling for Machine Learning Kernels”
Pure Fortran runs a production solver on NVIDIA
POT3D scales across multi-GPU nodes using only standard 'do concurrent' loops and unified memory.
Two views of a broken system turn out to be one cohomology class
Engineers can now translate between repair-style diagnosis and geometric computation of the same failure.
Verified inliner: 2.5x optimal
Rocq proof certifies inlining reaches a fixed point in bounded steps, at most 2.5 times the optimal cost.
· “Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics”
Testing whether spec-deltas beat code PRs for lakehouse changes
The paper formalizes a requirements-delta unit and designs a controlled experiment measuring time, defects, metric divergence, and…
Executable specs can pull software out of test-and-debug quicksand
Writing executable partial specs alongside code sharpens tests today and opens a gradual path from testing to proof
Static analysis soundly bounds adaptivity of data analyses
Round counts tell analysts which mechanism best controls generalization error.
1.2K synthetic terminal tasks lift agent scores by 6.75–8.24 points
Grounding instruction, solution, and verifier in the same realized container state makes 1.2K trajectories enough.
· “FACET: Preserving Source Intent and Executable State in Terminal Task Synthesis”
Certified 3-SAT filter: emptiness proves UNSAT
A proof assistant settles when triplet-intersection emptiness is a certified UNSAT answer and when it is not.
Tectonic compile success swings just 0.9 points across OSes
Classic TeX engines move 12–20 points with distribution policy; ETB isolates the cause.
· “Engine-Transfer-Bench: An Evidence-Based Benchmark for Document Compilation Engine Selection”
29.4x speedup on WebAssembly
Staging a concolic interpreter into C++ removes interpretation overhead; continuation snapshots skip re-execution.
Bilingual DSL turns one scheme into CPU and GPU code
Physics stays in C/C++; the compiler fuses both worlds in MLIR and replaces hundreds of handwritten lines with tens.
· “DSLHyPE-a DSL kernel language for the Exascale Hyperbolic PDE Engine ExaHyPE”
One rule decides every totality question in grounded arithmetic
OGA gives every totality question a certified yes-or-no status and reclassifies its Gödel sentence as a safe, priced fiction.
27 consensus divergences found by spec-guided fuzzing
Official tests miss boundary bugs that a mechanized spec's explicit if-premises expose.
· “SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients”
Graph surgery and mechanism replacement remove the same arrows
For acyclic causal models, the graphical and functional descriptions of intervention now match, and the proof is machine-checked.
· “Graph Surgery and the Do-Operator: A Precise Correspondence for Acyclic Structural Causal Models”
Posits fail to replace double precision in chaotic N-body test
One Posit library matches fp64's precision but runs ~1000x slower; the other errs ~10x more.
More AI code means higher stakes for good specs
The Specification Paradox: smarter code generators make correct, verifiable requirements more consequential, not less.
· “The Specification Paradox: Rethinking Requirements Engineering in the Age of AI”
Full-strength arithmetic defines its own truth predicate
Machine-checked proofs close the square: what RGA proves, it affirms true and provable from within.
Open-weight agent fixes 374 of 500 SWE-bench issues
Eight independent runs cross-apply each other's tests to pick the patch, with no fine-tuning and no hidden-test peeking.
· “Kozuchi Agent: A Language-Agnostic Open-Weight Agent for Software Repair”
Rust beats layered C retrofits in 7 of 9 benchmarks
Even the strongest C retrofit stacks miss one memory-safety class and pay 1.5x to 4.5x runtime penalties.
LLM rewrites with verification hit 83% accuracy and 16% speedup
A syntax, bounded-model-check, and LLM review chain lets an AI optimizer keep only the loop rewrites it can justify.
· “T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework”
For bounded programs, stack fits peak live memory plus largest buffer
A tree-scan allocator with defragmentation hits the bound and cuts real eBPF stacks by more than 90 percent.
MicroPython and CircuitPython win prototyping
Board counts, questions, and benchmarks put Python in classrooms and prototypes, not in hard-real-time production.
· “MicroPython and CircuitPython: Pythons Quiet Takeover of IoT and Robotics”
The exact conflict set cuts AI fabrication from 79% to 7%
Handing back the minimal conflicting rule set stops weaker models from deleting real constraints and inventing solutions.
· “From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving”
Rust GPU kernels hit near-parity with hand-tuned CUDA and HIP
A rustc/LLVM pipeline derives data movement from ownership types, hitting near-parity with CUDA/HIP kernels.
Barrier-free loop sync cuts AI accelerator latency 10-45%
Engines stall only for true data dependencies; the scheme comes with a machine-checked correctness proof.
· “A Barrier-Free Synchronization Algorithm for Multi-Engine AI Accelerators”
A transformer maps probabilistic programs to their Pareto fronts
A program-level calculus handles infinite-state MDPs symbolically, replacing finite-state enumeration with proof rules.
· “Multiobjective Preexpectation Reasoning for Probabilistic Programs”
One construction keeps noisy-stream monitors memory-bounded
Slack variables carry sensor error symbolically; an SMT offline pass catches violations online monitors miss.
· “Stream-based Online and Offline Monitoring under Measurement Noise”
125 bugs found in Ghidra's processor specs
Spec-driven testing against real hardware exposes silent decoding and semantic errors.
· “InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy”
Bounded symbolic runs plus LP yield sound cost bounds
Exhaustive exploration up to a chosen input size makes the fitted upper bounds provably safe in that range.
Rig equations between types give correct conversions
A commutative rig models algebraic data types, so every derivation yields a correct-by-construction converter to a packed layout.
SQL can shed nulls and duplicates without losing power
It debunks the excuses for nulls and bag semantics and shows what set-only query languages gain.
New tool filters 47.7% of mutually inconsistent Datalog alarms
PPProbe turns derivation graphs into Boolean constraints and enumerates the minimal conflict sets that generic MUS tools miss.
Dependency graph, not embeddings, chooses LLM context in IDE tool
Six code fixtures gave identical prompt tokens on three LLM families, with every callee traceable to a visible graph node.
Treat programs as operators to get optimal cost recurrences
A Galois-connection framework extracts optimal, solver-independent recurrences for catamorphic size metrics.
· “Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis”
Bounded windows restore safe splitting to 91 of 95 token sets
A scanner can prove where the current token began after a few bytes, so parallel chunks need no speculation.
· “Certified Split Windows for Parallel Lexing: Recovering Boundaries Where No Byte Certifies”
Cost is both monad and comonad in sound amortized typing
A single adjunction makes the same graded functor add and split cost, enabling compositional amortized analysis.
· “Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential”
Deciding if an ancilla can be uncomputed is coNP-hard
A rewrite-based tool can still uncompute clean and dirty ancillas on all 17 practical benchmarks.
Plan code and proof together
A shared program-and-proof plan beats write-then-prove across four LLMs and three Lean benchmarks.
· “P³: Joint Program-and-Proof Planning for Verified Code Generation”
Disjunctive security forces a choice: renaming or tightness
The universal type object splits; only deferred specialisation certifies the true bound for reused sources.
· “Renaming or Tightness: Enforcing Disjunctive Information Flow Policies”
Verified UPER parser reveals 20 flaws in 11 ASN.1 implementations
A formally verified parser becomes a reference oracle, catching bugs consensus testing misses.
Bona reuses 99% of dirty ancillas in quantum circuits
The scheduling problem is NP-hard; a depth-aware heuristic still matches clean-ancilla width with lower depth.
· “Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits”
Laziness lets HMC sample infinite-dimensional models
Gradient support and acceptance ratios stay finite even when the parameter space is infinite.
· “LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs”
SimP cuts compiler-bug reduction time by 1.75x
Switching to LLM reasoning when progress stalls keeps bugs small while saving about an hour per case.
· “SimP: Unifying Syntax- and Semantic-Guided Techniques for Efficient Program Reduction”
Irregular GPU kernels put Triton 11–31x behind CUDA C++
On a hash-blocked reconstruction kernel, Rust nears CUDA parity; both costs come from language limits.
· “What Irregularity Costs: CUDA C++, Rust, and Triton on a Hash-Blocked GPU Workload”
Recursive oracles compile with cleanup linear in recursion depth
Write oracles in classical style; the compiler adds register isolation and recursion-aware uncomputation automatically.
· “ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation”
Velosiraptor turns hardware specs into verified OS memory code
One high-level specification yields addmap, setperms, delmap, and a simulator-side MMU, checked by an SMT solver.
Combine source and IR embeddings to cut error to 1.54%
LLMCompiler embeddings beat graph models on POJ-104; device mapping stays competitive.
· “LLM-Based Embeddings for Program Analysis and Optimization”
Tracking classifier scopes blocks scope extrusion in staged code
Safe nested code generation, runtime execution, and cross-stage persistence with mutable state.
One reduction proof handles all weak isolation levels
A hierarchy of abstract models lets any new protocol prove its isolation level by one refinement, with no ad-hoc reduction.
· “Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions”
Python taint analysis hits top recall with generic IFDS engine
PyFlow's reusable solver finds 85.8% of synthetic and 48.1% of real-world Python vulnerabilities, beating eight SAST tools.
· “PyFlow: An Inter-procedural Static Analysis Framework for Python”
New logic verifies and synthesizes quantum programs for noisy chips
By tracking full state distributions instead of averages, it beats textbook programs on real noisy hardware.
· “Noise-aware Verification and Synthesis of Quantum Programs”
Agent learns DSL grammars from logs with near-perfect precision
Execution logs become validation grammars that match professional grammars on real query tasks.
Split verification logic across two theories
Dividing bit-precise verification problems into integer and bit-vector fragments with sound bridges yields large speedups.
· “Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning”
Adding one primitive makes LLM app flows probabilistic
With a factor statement scoring each trace, one PPDL program runs voting, importance sampling, or SMC unchanged.
Datalog's least model becomes an annealer's ground state
A four-stage compiler makes a Datalog program's least model the unique low-energy state of an Ising Hamiltonian.
Mixing error-correction codes cuts fault-tolerant quantum costs
A compositional tool reports space, time, and error for programs mixing quantum error-correcting codes.
Compiler passes can speed up pointer analysis 3.14x
Running standard optimizations before analysis cuts time and memory on real C/C++ code with little precision loss.
· “Accelerating C/C++ Pointer Analysis via Compiler-Based Offline Simplifications”
Step through FRP source, not generated C
Emdb maps Emfrp constructs onto generated C lines, enabling node-level stepping, watchpoints, and input-trace replay on a microcontroller.
Best LLM recovers compiler-missed speedups on 83% of attempts
On a 120-case benchmark, the top model turns hidden program facts into contract-safe rewrites that beat -O3/LTO/PGO
· “Can Large Language Models Recover Semantic Optimization Opportunities That Compilers Miss?”
Compatible code-agent layers make prompt swaps provably safe
A local check at each pipeline stage composes into an end-to-end guarantee for AI code generation.
· “GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation”
Regex lookaheads compile away: automaton needs 2^{2^m} states
Positive and negative lookaheads compile into automata, making matching linear in string length.
· “Translation of Regular Expression with Lookahead into Finite State Automaton”
Synthesized mini-programs shrink checkpoints by 34%
A per-tensor reversible program regenerates every bit, beating zstd, gzip, and tensor-specific codecs.
Digital twin catches all three planted AArch64 bugs
One-pass automata match rules against execution traces, explaining each hit with actual register and memory values.
· “Vulnerability Detection in AArch64 Machine Code Using a Digital Twin”
Parser checks drop from a day to minutes
Octopus symbolically bisimulates parser automata and returns a certificate or a counterexample bit-stream, running on consumer hardware.
· “Octopus: Practical Equivalence Checking of P4 Packet Parsers”
A 34-KLOC compiler trains and deploys through Vulkan and Metal
On five consumer GPUs it wins 12 of 20 minimal-latency cells and rivals vendor stacks on AMD.
· “Meganeura: Portable GPU Training and Inference through Vulkan and Metal”
